changeset 45620 | f2a587696afb |
parent 45602 | 2a858377c3d2 |
child 45625 | 750c5a47400b |
--- a/src/ZF/pair.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/ZF/pair.thy Wed Nov 23 22:59:39 2011 +0100 @@ -12,7 +12,7 @@ setup {* Simplifier.map_simpset_global (fn ss => ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) - addcongs [@{thm if_weak_cong}]) + |> Simplifier.add_cong @{thm if_weak_cong}) *} ML {* val ZF_ss = @{simpset} *}