src/ZF/OrdQuant.thy
changeset 26339 7825c83c9eff
parent 24893 b8ef7afe3a6b
child 26480 544cef16045b
     1.1 --- a/src/ZF/OrdQuant.thy	Wed Mar 19 22:28:17 2008 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed Mar 19 22:47:35 2008 +0100
     1.3 @@ -362,7 +362,9 @@
     1.4      atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
     1.5                   ZF_conn_pairs,
     1.6               ZF_mem_pairs);
     1.7 -change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
     1.8 +*}
     1.9 +declaration {* fn _ =>
    1.10 +  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    1.11  *}
    1.12  
    1.13  text {* Setting up the one-point-rule simproc *}