src/HOL/HOL.thy
changeset 42795 66fcc9882784
parent 42477 52fa26b6c524
child 42799 4e33894aec6d
     1.1 --- a/src/HOL/HOL.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -1205,7 +1205,7 @@
     1.4  use "Tools/simpdata.ML"
     1.5  ML {* open Simpdata *}
     1.6  
     1.7 -setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     1.8 +setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
     1.9  
    1.10  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    1.11  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}