# HG changeset patch
# User wenzelm
# Date 1305321846 -7200
# Node ID 07155da3b2f475000e5ba05d6ed6b4bcefb832e5
# Parent  88bee9f6eec7408af1ab736863ab7b7184e209f9
make ZF_cs snapshot after final setup;

diff -r 88bee9f6eec7 -r 07155da3b2f4 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri May 13 22:55:00 2011 +0200
+++ b/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
@@ -1,7 +1,6 @@
 (*  Title:      ZF/pair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
 
 header{*Ordered Pairs*}
@@ -10,6 +9,14 @@
 uses "simpdata.ML"
 begin
 
+declaration {*
+  fn _ => Simplifier.map_ss (fn ss =>
+    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
+    addcongs [@{thm if_weak_cong}])
+*}
+
+ML {* val ZF_ss = @{simpset} *}
+
 simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
   let
     val unfold_bex_tac = unfold_tac @{thms Bex_def};
diff -r 88bee9f6eec7 -r 07155da3b2f4 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Fri May 13 22:55:00 2011 +0200
+++ b/src/ZF/simpdata.ML	Fri May 13 23:24:06 2011 +0200
@@ -43,9 +43,3 @@
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
-change_simpset (fn ss =>
-  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
-  addcongs [@{thm if_weak_cong}]);
-
-val ZF_ss = @{simpset};
-