src/ZF/pair.thy
changeset 42795 66fcc9882784
parent 42794 07155da3b2f4
child 45602 2a858377c3d2
     1.1 --- a/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  uses "simpdata.ML"
     1.5  begin
     1.6  
     1.7 -declaration {*
     1.8 -  fn _ => Simplifier.map_ss (fn ss =>
     1.9 +setup {*
    1.10 +  Simplifier.map_simpset_global (fn ss =>
    1.11      ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    1.12      addcongs [@{thm if_weak_cong}])
    1.13  *}