src/ZF/OrdQuant.thy
changeset 17876 b9c92f384109
parent 17002 fb9261990ffe
child 18324 d1c4b1112e33
     1.1 --- a/src/ZF/OrdQuant.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4      atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
     1.5                   ZF_conn_pairs,
     1.6               ZF_mem_pairs);
     1.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     1.8 +change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
     1.9  *}
    1.10  
    1.11  text {* Setting up the one-point-rule simproc *}