src/HOL/HOL.ML
changeset 3621 d3e248853428
parent 3615 e5322197cfea
child 3646 a11338a5d2d4
--- a/src/HOL/HOL.ML	Wed Aug 06 11:56:31 1997 +0200
+++ b/src/HOL/HOL.ML	Wed Aug 06 11:57:20 1997 +0200
@@ -349,14 +349,11 @@
      _ $ (Const("op -->",_)$_$_) => th RS mp
   | _ => raise THM("RSmp",0,[th]));
 
-(*Used in qed_spec_mp, etc.*)
 fun normalize_thm funs =
 let fun trans [] th = th
       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
 in trans funs end;
 
-end;
-
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())
   in bind_thm(name, thm) end;
@@ -367,6 +364,9 @@
 fun qed_goalw_spec_mp name thy defs s p = 
 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
 
+end;
+
+
 (*Thus, assignments to the references claset and simpset are recorded
   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
 use "hologic.ML";