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