# HG changeset patch
# User wenzelm
# Date 1737200604 -3600
# Node ID cd9df61fee349b5e6ae719290d924279dad2dcb8
# Parent  705770ff7fb35f7297cd1737e605a33743222423
tuned source structure;

diff -r 705770ff7fb3 -r cd9df61fee34 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Jan 18 12:25:23 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Sat Jan 18 12:43:24 2025 +0100
@@ -31,6 +31,10 @@
 structure Import_Rule: IMPORT_RULE =
 struct
 
+(** primitive rules of HOL Light **)
+
+(* basic logic *)
+
 fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
 
 fun meta_mp th1 th2 =
@@ -145,6 +149,9 @@
     meta_mp i th2
   end
 
+
+(* instantiation *)
+
 fun freezeT thy th =
   let
     fun add (v as ((a, _), S)) tvars =
@@ -168,6 +175,26 @@
     Thm.instantiate (TVars.empty, inst) th
   end)
 
+fun inst_type lambda =
+  let
+    val tyinst =
+      TFrees.build (lambda |> fold (fn (a, b) =>
+        TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
+  in
+    Thm.instantiate_frees (tyinst, Frees.empty)
+  end
+
+fun inst sigma th =
+  let
+    val (dom, rng) = ListPair.unzip (rev sigma)
+  in
+    th |> forall_intr_list dom
+       |> forall_elim_list rng
+  end
+
+
+(* constant definitions *)
+
 fun def' c rhs thy =
   let
     val b = Binding.name c
@@ -190,6 +217,9 @@
     (warning ("Const mapped, but def provided: " ^ quote c); (mdef thy c, thy))
   else def' c (Thm.term_of rhs) thy
 
+
+(* type definitions *)
+
 fun typedef_hol2hollight A B rep abs pred a r =
   Thm.instantiate' [SOME A, SOME B] [SOME rep, SOME abs, SOME pred, SOME a, SOME r]
     @{lemma "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
@@ -249,22 +279,11 @@
     (warning ("Type mapped but proofs provided: " ^ quote tycname); (mtydef thy tycname, thy))
   else tydef' tycname abs_name rep_name P t td_th thy
 
-fun inst_type lambda =
-  let
-    val tyinst =
-      TFrees.build (lambda |> fold (fn (a, b) =>
-        TFrees.add (Term.dest_TFree (Thm.typ_of a), b)))
-  in
-    Thm.instantiate_frees (tyinst, Frees.empty)
-  end
+
 
-fun inst sigma th =
-  let
-    val (dom, rng) = ListPair.unzip (rev sigma)
-  in
-    th |> forall_intr_list dom
-       |> forall_elim_list rng
-  end
+(** importer **)
+
+(* basic entities *)
 
 val make_name = String.translate (fn #"." => "dot" | c => Char.toString c)
 
@@ -295,6 +314,10 @@
 val assume_thm = Thm.trivial o Thm.apply \<^cterm>\<open>Trueprop\<close>
 
 
+(* import file *)
+
+local
+
 datatype state =
   State of theory * (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
 
@@ -394,6 +417,8 @@
   | command (#"+", [s]) = store_last_thm (Binding.name (make_name s))
   | command (c, _) = raise Fail ("process: unknown command: " ^ String.str c)
 
+in
+
 fun import_file path0 thy =
   let
     val path = File.absolute_path (Resources.master_directory thy + path0)
@@ -407,3 +432,5 @@
     (Parse.path >> (fn name => Toplevel.theory (fn thy => import_file (Path.explode name) thy)))
 
 end
+
+end