src/ZF/OrdQuant.thy
changeset 36543 0e7fc5bf38de
parent 35112 ff6f60e6ab85
child 38715 6513ea67d95d
     1.1 --- a/src/ZF/OrdQuant.thy	Thu Apr 29 22:08:57 2010 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Thu Apr 29 22:56:32 2010 +0200
     1.3 @@ -363,7 +363,7 @@
     1.4               ZF_mem_pairs);
     1.5  *}
     1.6  declaration {* fn _ =>
     1.7 -  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
     1.8 +  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
     1.9  *}
    1.10  
    1.11  text {* Setting up the one-point-rule simproc *}