src/ZF/Main_ZF.thy
changeset 26339 7825c83c9eff
parent 26056 6a0801279f4c
child 29580 117b88da143c
--- a/src/ZF/Main_ZF.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/ZF/Main_ZF.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -72,8 +72,8 @@
 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
 
 
-ML_setup {*
-  change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
 *}
 
 end