| changeset 36543 | 0e7fc5bf38de |
| parent 29580 | 117b88da143c |
| child 45625 | 750c5a47400b |
--- a/src/ZF/Main_ZF.thy Thu Apr 29 22:08:57 2010 +0200 +++ b/src/ZF/Main_ZF.thy Thu Apr 29 22:56:32 2010 +0200 @@ -71,7 +71,7 @@ declaration {* fn _ => - Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all)) + Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all))) *} end