1.1 --- a/src/ZF/pair.thy	Fri May 13 22:55:00 2011 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      ZF/pair.thy
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8  *)
     1.9  
    1.10  header{*Ordered Pairs*}
    1.11 @@ -10,6 +9,14 @@
    1.12  uses "simpdata.ML"
    1.13  begin
    1.14  
    1.15 +declaration {*
    1.16 +  fn _ => Simplifier.map_ss (fn ss =>
    1.17 +    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    1.18 +    addcongs [@{thm if_weak_cong}])
    1.19 +*}
    1.20 +
    1.21 +ML {* val ZF_ss = @{simpset} *}
    1.22 +
    1.23  simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
    1.24    let
    1.25      val unfold_bex_tac = unfold_tac @{thms Bex_def};

     2.1 --- a/src/ZF/simpdata.ML	Fri May 13 22:55:00 2011 +0200
     2.2 +++ b/src/ZF/simpdata.ML	Fri May 13 23:24:06 2011 +0200
     2.3 @@ -43,9 +43,3 @@
     2.4  
     2.5  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
     2.6  
     2.7 -change_simpset (fn ss =>
     2.8 -  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     2.9 -  addcongs [@{thm if_weak_cong}]);
    2.10 -
    2.11 -val ZF_ss = @{simpset};
    2.12 -