From a5692e0ba36b372b9175d7b356f4b2fd1ee3d663 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 11 Feb 2019 15:37:18 +0100
Subject: Put typing functionality into a .thy and clean up antiquotations,
 which results in some reorganization of the theory import structure.

---
 util.ML | 72 +++++++++++++++++++++++++++++++++--------------------------------
 1 file changed, 37 insertions(+), 35 deletions(-)

(limited to 'util.ML')

diff --git a/util.ML b/util.ML
index c2e962b..f7aab9a 100644
--- a/util.ML
+++ b/util.ML
@@ -28,6 +28,7 @@ end
 structure Util: UTIL =
 struct
 
+(* Unmark a name string identifier *)
 fun unmark s =
   Lexicon.unmark_class s
   handle Fail "unprefix" =>
@@ -39,40 +40,6 @@ fun unmark s =
   handle Fail "unprefix" =>
   s
 
-fun name_and_thm (fact, thm) =
-  ((case fact of
-    Facts.Named ((name, _), _) => name
-  | Facts.Fact name => name),
-  thm)
-
-fun get_all_thms ctxt =
-  let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
-  in ref_thms |> (map name_and_thm)
-  end
-
-(* Search all visible theorems (including local assumptions) containing a given name *)
-fun find_thm ctxt name =
-  let val (_, ref_thms) =
-    Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
-  in
-    ref_thms |> (map name_and_thm)
-  end
-
-(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
-fun get_this ctxt =
-  Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
-    |> Proof_Context.lookup_fact ctxt |> the |> #thms
-  handle Option.Option => (
-    if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
-    []
-  )
-
-(* Get all visible assumptions in the current proof scope.
-   This includes the facts introduced in the statement of the goal using "assumes",
-   as well as all facts introduced using "assume" that are visible in the current block.
- *)
-val get_assms = Assumption.all_prems_of
-
 (* Prepare a Pure pre-term, converting it to a (unchecked) term *)
 fun prep_term ctxt ptm =
   let val ptm = Term_Position.strip_positions ptm
@@ -119,4 +86,39 @@ fun string_of_term tm =
   | Abs (_, typ, body) => "Abs (_, " ^ string_of_typ typ ^ ", " ^ string_of_term body ^ ")"
   | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
 
-end
\ No newline at end of file
+fun name_and_thm (fact, thm) =
+  ((case fact of
+    Facts.Named ((name, _), _) => name
+  | Facts.Fact name => name),
+  thm)
+
+(* Return all visible theorems *)
+fun get_all_thms ctxt =
+  let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
+  in ref_thms |> (map name_and_thm)
+  end
+
+(* Search all visible theorems (including local assumptions) containing a given name *)
+fun find_thm ctxt name =
+  let val (_, ref_thms) =
+    Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
+  in
+    ref_thms |> (map name_and_thm)
+  end
+
+(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
+fun get_this ctxt =
+  Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
+    |> Proof_Context.lookup_fact ctxt |> the |> #thms
+  handle Option.Option => (
+    if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
+    []
+  )
+
+(* Get all visible assumptions in the current proof scope.
+   This includes the facts introduced in the statement of the goal using "assumes",
+   as well as all facts introduced using "assume" that are visible in the current block.
+ *)
+val get_assms = Assumption.all_prems_of
+
+end
-- 
cgit v1.2.3