src/ZF/pair.thy

--- a/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/ZF/pair.thy	Fri May 13 23:58:40 2011 +0200
@@ -9,8 +9,8 @@
 uses "simpdata.ML"
 begin
 
-declaration {*
-  fn _ => Simplifier.map_ss (fn ss =>
+setup {*
+  Simplifier.map_simpset_global (fn ss =>
     ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     addcongs [@{thm if_weak_cong}])
 *}