src/ZF/pair.thy

--- 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} *}