# HG changeset patch
# User sandnerr
# Date 850154846 -3600
# Node ID 7405e3cac88ae04c2cab12c82d9aafed5f874ba6
# Parent  562cb286138e7a8443f5c3977d2913a8f8253bcd
qed_spec_mp moved to end of file

diff -r 562cb286138e -r 7405e3cac88a src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Mon Dec 09 16:51:14 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Mon Dec 09 19:07:26 1996 +0100
@@ -10,10 +10,6 @@
 val banner = "HOLCF with sections axioms,ops,domain,generated";
 init_thy_reader();
 
-fun qed_spec_mp name =
-  let val thm = normalize_thm [RSspec,RSmp] (result())
-  in bind_thm(name, thm) end;
-
 (* start 8bit 1 *)
 val banner = 
         "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
@@ -47,4 +43,8 @@
 print_depth 100;  
 make_html:=false;
 
+fun qed_spec_mp name =
+  let val thm = normalize_thm [RSspec,RSmp] (result())
+  in bind_thm(name, thm) end;
+
 val HOLCF_build_completed = (); (*indicate successful build*)