src/ZF/pair.thy
changeset 51717 9e7d1c139569
parent 48891 c0eafbd55de3
child 54998 8601434fa334
     1.1 --- a/src/ZF/pair.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/ZF/pair.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -11,25 +11,25 @@
     1.4  ML_file "simpdata.ML"
     1.5  
     1.6  setup {*
     1.7 -  Simplifier.map_simpset_global
     1.8 +  map_theory_simpset
     1.9      (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
    1.10        #> Simplifier.add_cong @{thm if_weak_cong})
    1.11  *}
    1.12  
    1.13 -ML {* val ZF_ss = @{simpset} *}
    1.14 +ML {* val ZF_ss = simpset_of @{context} *}
    1.15  
    1.16  simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
    1.17    let
    1.18      val unfold_bex_tac = unfold_tac @{thms Bex_def};
    1.19 -    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.20 -  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
    1.21 +    fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
    1.22 +  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
    1.23  *}
    1.24  
    1.25  simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
    1.26    let
    1.27      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.28 -    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.29 -  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
    1.30 +    fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
    1.31 +  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
    1.32  *}
    1.33  
    1.34