src/ZF/pair.thy
changeset 45625 750c5a47400b
parent 45620 f2a587696afb
child 46820 c656222c4dc1
     1.1 --- a/src/ZF/pair.thy	Thu Nov 24 20:45:34 2011 +0100
     1.2 +++ b/src/ZF/pair.thy	Thu Nov 24 21:01:06 2011 +0100
     1.3 @@ -10,9 +10,9 @@
     1.4  begin
     1.5  
     1.6  setup {*
     1.7 -  Simplifier.map_simpset_global (fn ss =>
     1.8 -    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     1.9 -    |> Simplifier.add_cong @{thm if_weak_cong})
    1.10 +  Simplifier.map_simpset_global
    1.11 +    (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
    1.12 +      #> Simplifier.add_cong @{thm if_weak_cong})
    1.13  *}
    1.14  
    1.15  ML {* val ZF_ss = @{simpset} *}