src/HOL/Set.thy
changeset 26339 7825c83c9eff
parent 26150 f6bd8686b71e
child 26480 544cef16045b
     1.1 --- a/src/HOL/Set.thy	Wed Mar 19 22:28:17 2008 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Mar 19 22:47:35 2008 +0100
     1.3 @@ -428,8 +428,8 @@
     1.4    Gives better instantiation for bound:
     1.5  *}
     1.6  
     1.7 -ML_setup {*
     1.8 -  change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
     1.9 +declaration {* fn _ =>
    1.10 +  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
    1.11  *}
    1.12  
    1.13  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
    1.14 @@ -1031,9 +1031,11 @@
    1.15     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
    1.16   *)
    1.17  
    1.18 -ML_setup {*
    1.19 +ML {*
    1.20    val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
    1.21 -  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    1.22 +*}
    1.23 +declaration {* fn _ =>
    1.24 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
    1.25  *}
    1.26  
    1.27