src/HOL/Set.thy
changeset 45625 750c5a47400b
parent 45607 16b4f5774621
child 45651 172aa230ce69
--- a/src/HOL/Set.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Set.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -369,7 +369,7 @@
 *}
 
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
 *}
 
 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"