moved setmksimps to Main!
authorwenzelm
Fri, 11 Jan 2002 00:34:43 +0100
changeset 12715 f7299128cd7d
parent 12714 61af28328417
child 12716 fa4ea2856a31
moved setmksimps to Main!
src/ZF/Main.ML
src/ZF/ROOT.ML
--- a/src/ZF/Main.ML	Fri Jan 11 00:33:35 2002 +0100
+++ b/src/ZF/Main.ML	Fri Jan 11 00:34:43 2002 +0100
@@ -3,3 +3,5 @@
 struct
   val thy = the_context ();
 end;
+
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
--- a/src/ZF/ROOT.ML	Fri Jan 11 00:33:35 2002 +0100
+++ b/src/ZF/ROOT.ML	Fri Jan 11 00:34:43 2002 +0100
@@ -22,7 +22,6 @@
 use "~~/src/Provers/Arith/combine_numerals.ML";
 
 with_path "Integ" use_thy "Main_ZFC";
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
 
 print_depth 8;