avoid referencing thy value;
authorwenzelm
Mon Jul 24 23:51:46 2000 +0200 (2000-07-24)
changeset 94224b6bc2b347e5
parent 9421 d8dfa816a368
child 9423 7aa79267fa82
avoid referencing thy value;
src/HOL/Fun.ML
src/HOL/Gfp.ML
src/HOL/Integ/IntDiv.ML
src/HOL/Lfp.ML
src/HOL/Ord.ML
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/PNat.ML
src/HOL/Real/RealDef.ML
src/HOL/Set.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/Vimage.ML
src/HOL/WF.ML
src/HOL/WF_Rel.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Fun.ML	Mon Jul 24 23:51:11 2000 +0200
     1.2 +++ b/src/HOL/Fun.ML	Mon Jul 24 23:51:46 2000 +0200
     1.3 @@ -460,12 +460,13 @@
     1.4            if v aconv x then Some g else gen_fun_upd (find g) T v w
     1.5        |   find t = None
     1.6        in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
     1.7 +  val ss = simpset ();
     1.8    val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
     1.9 -                          simp_tac (simpset_of Fun.thy) 1]
    1.10 +                          simp_tac ss 1]
    1.11    fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
    1.12  in 
    1.13    val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
    1.14 -   [Thm.read_cterm (sign_of Fun.thy) ("f(v:=w,x:=y)", HOLogic.termT)] 
    1.15 +   [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
    1.16     (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
    1.17         Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
    1.18  end;
     2.1 --- a/src/HOL/Gfp.ML	Mon Jul 24 23:51:11 2000 +0200
     2.2 +++ b/src/HOL/Gfp.ML	Mon Jul 24 23:51:46 2000 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/gfp
     2.5 +(*  Title:      HOL/Gfp.ML
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1993  University of Cambridge
     2.9 @@ -6,8 +6,6 @@
    2.10  The Knaster-Tarski Theorem for greatest fixed points.
    2.11  *)
    2.12  
    2.13 -open Gfp;
    2.14 -
    2.15  (*** Proof of Knaster-Tarski Theorem using gfp ***)
    2.16  
    2.17  (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    2.18 @@ -16,7 +14,7 @@
    2.19  by (etac (CollectI RS Union_upper) 1);
    2.20  qed "gfp_upperbound";
    2.21  
    2.22 -val prems = goalw Gfp.thy [gfp_def]
    2.23 +val prems = goalw (the_context ()) [gfp_def]
    2.24      "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
    2.25  by (REPEAT (ares_tac ([Union_least]@prems) 1));
    2.26  by (etac CollectD 1);
    2.27 @@ -44,7 +42,7 @@
    2.28  by Auto_tac;
    2.29  qed "weak_coinduct";
    2.30  
    2.31 -val [prem,mono] = goal Gfp.thy
    2.32 +val [prem,mono] = goal (the_context ())
    2.33      "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
    2.34  \    X Un gfp(f) <= f(X Un gfp(f))";
    2.35  by (rtac (prem RS Un_least) 1);
    2.36 @@ -59,7 +57,7 @@
    2.37  by (REPEAT (ares_tac [UnI1, Un_least] 1));
    2.38  qed "coinduct";
    2.39  
    2.40 -val [mono,prem] = goal Gfp.thy
    2.41 +val [mono,prem] = goal (the_context ())
    2.42      "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
    2.43  by (rtac (mono RS mono_Un RS subsetD) 1);
    2.44  by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1);
    2.45 @@ -74,7 +72,7 @@
    2.46  by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
    2.47  qed "coinduct3_mono_lemma";
    2.48  
    2.49 -val [prem,mono] = goal Gfp.thy
    2.50 +val [prem,mono] = goal (the_context ())
    2.51      "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
    2.52  \    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
    2.53  by (rtac subset_trans 1);
    2.54 @@ -98,12 +96,12 @@
    2.55  
    2.56  (** Definition forms of gfp_Tarski and coinduct, to control unfolding **)
    2.57  
    2.58 -val [rew,mono] = goal Gfp.thy "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
    2.59 +val [rew,mono] = goal (the_context ()) "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
    2.60  by (rewtac rew);
    2.61  by (rtac (mono RS gfp_Tarski) 1);
    2.62  qed "def_gfp_Tarski";
    2.63  
    2.64 -val rew::prems = goal Gfp.thy
    2.65 +val rew::prems = goal (the_context ())
    2.66      "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
    2.67  by (rewtac rew);
    2.68  by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
    2.69 @@ -118,7 +116,7 @@
    2.70  by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
    2.71  qed "def_Collect_coinduct";
    2.72  
    2.73 -val rew::prems = goal Gfp.thy
    2.74 +val rew::prems = goal (the_context ())
    2.75      "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
    2.76  by (rewtac rew);
    2.77  by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
     3.1 --- a/src/HOL/Integ/IntDiv.ML	Mon Jul 24 23:51:11 2000 +0200
     3.2 +++ b/src/HOL/Integ/IntDiv.ML	Mon Jul 24 23:51:46 2000 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4  
     3.5  (*Proving negDivAlg's termination condition*)
     3.6  val [tc] = negDivAlg.tcs;
     3.7 -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
     3.8 +goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
     3.9  by Auto_tac;
    3.10  val lemma = result();
    3.11  
    3.12 @@ -425,7 +425,7 @@
    3.13  by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
    3.14  qed "mod_neg_neg";
    3.15  
    3.16 -Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
    3.17 +Addsimps (map (read_instantiate_sg (sign_of (the_context ()))
    3.18  	       [("a", "number_of ?v"), ("b", "number_of ?w")])
    3.19  	  [div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
    3.20  	   mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
    3.21 @@ -835,8 +835,7 @@
    3.22  \         (if ~b | (#0::int) <= number_of w                   \
    3.23  \          then number_of v div (number_of w)    \
    3.24  \          else (number_of v + (#1::int)) div (number_of w))";
    3.25 -by (simp_tac (simpset_of Int.thy
    3.26 -			 addsimps [zadd_assoc, number_of_BIT]) 1);
    3.27 +by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
    3.28  by (asm_simp_tac (simpset()
    3.29                    delsimps bin_arith_extra_simps@bin_rel_simps
    3.30  		  addsimps [zdiv_zmult_zmult1,
    3.31 @@ -895,8 +894,7 @@
    3.32  \               then #2 * (number_of v mod number_of w) + #1    \
    3.33  \               else #2 * ((number_of v + (#1::int)) mod number_of w) - #1  \
    3.34  \          else #2 * (number_of v mod number_of w))";
    3.35 -by (simp_tac (simpset_of Int.thy
    3.36 -			 addsimps [zadd_assoc, number_of_BIT]) 1);
    3.37 +by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
    3.38  by (asm_simp_tac (simpset()
    3.39  		  delsimps bin_arith_extra_simps@bin_rel_simps
    3.40  		  addsimps [zmod_zmult_zmult1,
     4.1 --- a/src/HOL/Lfp.ML	Mon Jul 24 23:51:11 2000 +0200
     4.2 +++ b/src/HOL/Lfp.ML	Mon Jul 24 23:51:46 2000 +0200
     4.3 @@ -1,13 +1,11 @@
     4.4 -(*  Title:      HOL/lfp.ML
     4.5 +(*  Title:      HOL/Lfp.ML
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1992  University of Cambridge
     4.9  
    4.10 -The Knaster-Tarski Theorem
    4.11 +The Knaster-Tarski Theorem.
    4.12  *)
    4.13  
    4.14 -open Lfp;
    4.15 -
    4.16  (*** Proof of Knaster-Tarski Theorem ***)
    4.17  
    4.18  (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
    4.19 @@ -57,7 +55,7 @@
    4.20  
    4.21  (** Definition forms of lfp_Tarski and induct, to control unfolding **)
    4.22  
    4.23 -val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
    4.24 +val [rew,mono] = goal (the_context ()) "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
    4.25  by (rewtac rew);
    4.26  by (rtac (mono RS lfp_Tarski) 1);
    4.27  qed "def_lfp_Tarski";
     5.1 --- a/src/HOL/Ord.ML	Mon Jul 24 23:51:11 2000 +0200
     5.2 +++ b/src/HOL/Ord.ML	Mon Jul 24 23:51:46 2000 +0200
     5.3 @@ -120,7 +120,7 @@
     5.4  by (Blast_tac 1);
     5.5  qed "linorder_less_linear";
     5.6  
     5.7 -val prems = goal thy
     5.8 +val prems = goal (the_context ())
     5.9   "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
    5.10  by(cut_facts_tac [linorder_less_linear] 1);
    5.11  by(REPEAT(eresolve_tac (prems@[disjE]) 1));
     6.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Mon Jul 24 23:51:11 2000 +0200
     6.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Mon Jul 24 23:51:46 2000 +0200
     6.3 @@ -342,7 +342,7 @@
     6.4  
     6.5  Addsimps [Compl_empty_eq];
     6.6  
     6.7 -val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
     6.8 +val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
     6.9  \            {A:: 'a set. finite (- A)} : Filter UNIV";
    6.10  by (cut_facts_tac [prem] 1);
    6.11  by (rtac mem_FiltersetI2 1);
    6.12 @@ -365,13 +365,13 @@
    6.13  by (Blast_tac 1);
    6.14  qed "not_finite_UNIV_Compl";
    6.15  
    6.16 -val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
    6.17 +val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
    6.18  \            !X: {A:: 'a set. finite (- A)}. ~ finite X";
    6.19  by (cut_facts_tac [prem] 1);
    6.20  by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
    6.21  qed "mem_cofinite_Filter_not_finite";
    6.22  
    6.23 -val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
    6.24 +val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
    6.25  \            {A:: 'a set. finite (- A)} : Freefilter UNIV";
    6.26  by (cut_facts_tac [prem] 1);
    6.27  by (rtac mem_FreefiltersetI2 1);
     7.1 --- a/src/HOL/Real/PNat.ML	Mon Jul 24 23:51:11 2000 +0200
     7.2 +++ b/src/HOL/Real/PNat.ML	Mon Jul 24 23:51:46 2000 +0200
     7.3 @@ -1,9 +1,9 @@
     7.4 -(*  Title       : PNat.ML
     7.5 +(*  Title       : HOL/Real/PNat.ML
     7.6      ID          : $Id$
     7.7      Author      : Jacques D. Fleuriot
     7.8      Copyright   : 1998  University of Cambridge
     7.9 -    Description : The positive naturals -- proofs 
    7.10 -                : mainly as in Nat.thy
    7.11 +
    7.12 +The positive naturals -- proofs mainly as in theory Nat.
    7.13  *)
    7.14  
    7.15  Goal "mono(%X. {1} Un (Suc``X))";
    7.16 @@ -30,14 +30,14 @@
    7.17  
    7.18  (*** Induction ***)
    7.19  
    7.20 -val major::prems = goal thy
    7.21 +val major::prems = goal (the_context ())
    7.22      "[| i: pnat;  P(1);   \
    7.23  \       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
    7.24  by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_induct) 1);
    7.25  by (blast_tac (claset() addIs prems) 1);
    7.26  qed "PNat_induct";
    7.27  
    7.28 -val prems = goalw thy [pnat_one_def,pnat_Suc_def]
    7.29 +val prems = goalw (the_context ()) [pnat_one_def,pnat_Suc_def]
    7.30      "[| P(1p);   \
    7.31  \       !!n. P(n) ==> P(pSuc n) |]  ==> P(n)";
    7.32  by (rtac (Rep_pnat_inverse RS subst) 1);   
    7.33 @@ -50,7 +50,7 @@
    7.34  fun pnat_ind_tac a i = 
    7.35    res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
    7.36  
    7.37 -val prems = goal thy
    7.38 +val prems = goal (the_context ())
    7.39      "[| !!x. P x 1p;  \
    7.40  \       !!y. P 1p (pSuc y);  \
    7.41  \       !!x y. [| P x y |] ==> P (pSuc x) (pSuc y)  \
    7.42 @@ -63,7 +63,7 @@
    7.43  qed "pnat_diff_induct";
    7.44  
    7.45  (*Case analysis on the natural numbers*)
    7.46 -val prems = goal thy 
    7.47 +val prems = goal (the_context ())
    7.48      "[| n=1p ==> P;  !!x. n = pSuc(x) ==> P |] ==> P";
    7.49  by (subgoal_tac "n=1p | (EX x. n = pSuc(x))" 1);
    7.50  by (fast_tac (claset() addSEs prems) 1);
    7.51 @@ -340,7 +340,7 @@
    7.52  by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1);
    7.53  qed "pnat_le_refl";
    7.54  
    7.55 -val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::pnat)";
    7.56 +val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::pnat)";
    7.57  by (dtac pnat_le_imp_less_or_eq 1);
    7.58  by (blast_tac (claset() addIs [pnat_less_trans]) 1);
    7.59  qed "pnat_le_less_trans";
    7.60 @@ -384,7 +384,7 @@
    7.61  by (simp_tac (simpset() addsimps [lemma]) 1);
    7.62  qed "Least_pnat_def";
    7.63  
    7.64 -val [prem1,prem2] = goalw thy [Least_pnat_def]
    7.65 +val [prem1,prem2] = goalw (the_context ()) [Least_pnat_def]
    7.66      "[| P(k::pnat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
    7.67  by (rtac select_equality 1);
    7.68  by (blast_tac (claset() addSIs [prem1,prem2]) 1);
    7.69 @@ -647,7 +647,7 @@
    7.70      simpset() addsimps [pnat_mult_left_commute]));
    7.71  qed "pnat_same_multI2";
    7.72  
    7.73 -val [prem] = goal thy
    7.74 +val [prem] = goal (the_context ())
    7.75      "(!!u. z = Abs_pnat(u) ==> P) ==> P";
    7.76  by (cut_inst_tac [("x1","z")] 
    7.77      (rewrite_rule [pnat_def] (Rep_pnat RS Abs_pnat_inverse)) 1);
    7.78 @@ -706,7 +706,7 @@
    7.79  qed "pnat_of_nat_less_iff";
    7.80  Addsimps [pnat_of_nat_less_iff RS sym];
    7.81  
    7.82 -goalw PNat.thy [pnat_mult_def,pnat_of_nat_def] 
    7.83 +Goalw [pnat_mult_def,pnat_of_nat_def] 
    7.84        "pnat_of_nat n1 * pnat_of_nat n2 = \
    7.85  \      pnat_of_nat (n1 * n2 + n1 + n2)";
    7.86  by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult,
     8.1 --- a/src/HOL/Real/RealDef.ML	Mon Jul 24 23:51:11 2000 +0200
     8.2 +++ b/src/HOL/Real/RealDef.ML	Mon Jul 24 23:51:46 2000 +0200
     8.3 @@ -35,7 +35,7 @@
     8.4  by (Blast_tac 1);
     8.5  qed "realrelE_lemma";
     8.6  
     8.7 -val [major,minor] = goal thy
     8.8 +val [major,minor] = goal (the_context ())
     8.9    "[| p: realrel;  \
    8.10  \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
    8.11  \                    |] ==> Q |] ==> Q";
    8.12 @@ -94,7 +94,7 @@
    8.13  by (Asm_full_simp_tac 1);
    8.14  qed "inj_real_of_preal";
    8.15  
    8.16 -val [prem] = goal thy
    8.17 +val [prem] = goal (the_context ())
    8.18      "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
    8.19  by (res_inst_tac [("x1","z")] 
    8.20      (rewrite_rule [real_def] Rep_real RS quotientE) 1);
     9.1 --- a/src/HOL/Set.ML	Mon Jul 24 23:51:11 2000 +0200
     9.2 +++ b/src/HOL/Set.ML	Mon Jul 24 23:51:46 2000 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/set
     9.5 +(*  Title:      HOL/Set.ML
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1991  University of Cambridge
     9.9 @@ -719,9 +719,9 @@
    9.10  (*Split ifs on either side of the membership relation.
    9.11  	Not for Addsimps -- can cause goals to blow up!*)
    9.12  bind_thm ("split_if_mem1", 
    9.13 -    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
    9.14 +    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
    9.15  bind_thm ("split_if_mem2", 
    9.16 -    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    9.17 +    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
    9.18  
    9.19  bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    9.20  		  split_if_mem1, split_if_mem2]);
    10.1 --- a/src/HOL/Trancl.ML	Mon Jul 24 23:51:11 2000 +0200
    10.2 +++ b/src/HOL/Trancl.ML	Mon Jul 24 23:51:46 2000 +0200
    10.3 @@ -254,7 +254,7 @@
    10.4  qed "trancl_induct";
    10.5  
    10.6  (*Another induction rule for trancl, incorporating transitivity.*)
    10.7 -val major::prems = goal thy
    10.8 +val major::prems = goal (the_context ())
    10.9   "[| (x,y) : r^+; \
   10.10  \    !!x y. (x,y) : r ==> P x y; \
   10.11  \    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
    11.1 --- a/src/HOL/Univ.ML	Mon Jul 24 23:51:11 2000 +0200
    11.2 +++ b/src/HOL/Univ.ML	Mon Jul 24 23:51:46 2000 +0200
    11.3 @@ -387,7 +387,7 @@
    11.4  by (Blast_tac 1);
    11.5  qed "Funs_mono";
    11.6  
    11.7 -val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
    11.8 +val [p] = goalw (the_context ()) [Funs_def] "(!!x. f x : S) ==> f : Funs S";
    11.9  by (rtac CollectI 1);
   11.10  by (rtac subsetI 1);
   11.11  by (etac rangeE 1);
   11.12 @@ -401,7 +401,7 @@
   11.13  by (rtac rangeI 1);
   11.14  qed "FunsD";
   11.15  
   11.16 -val [p1, p2] = goalw thy [o_def]
   11.17 +val [p1, p2] = goalw (the_context ()) [o_def]
   11.18    "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
   11.19  by (rtac (p2 RS ext) 1);
   11.20  by (rtac (p1 RS FunsD) 1);
    12.1 --- a/src/HOL/Vimage.ML	Mon Jul 24 23:51:11 2000 +0200
    12.2 +++ b/src/HOL/Vimage.ML	Mon Jul 24 23:51:46 2000 +0200
    12.3 @@ -79,7 +79,7 @@
    12.4  (*A strange result used in Tools/inductive_package*)
    12.5  bind_thm ("vimage_Collect", 
    12.6  	  allI RS 
    12.7 -	  prove_goalw thy [vimage_def]
    12.8 +	  prove_goalw (the_context ()) [vimage_def]
    12.9  	  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
   12.10  	      (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
   12.11  
    13.1 --- a/src/HOL/WF.ML	Mon Jul 24 23:51:11 2000 +0200
    13.2 +++ b/src/HOL/WF.ML	Mon Jul 24 23:51:46 2000 +0200
    13.3 @@ -275,7 +275,7 @@
    13.4  qed_spec_mp "is_recfun_equal";
    13.5  
    13.6  
    13.7 -val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
    13.8 +val prems as [wfr,transr,recfa,recgb,_] = goalw (the_context ()) [cut_def]
    13.9      "[| wf(r);  trans(r); \
   13.10  \       is_recfun r H a f;  is_recfun r H b g;  (b,a):r |] ==> \
   13.11  \    cut f r b = g";
   13.12 @@ -342,7 +342,7 @@
   13.13  (*---------------------------------------------------------------------------
   13.14   * This form avoids giant explosions in proofs.  NOTE USE OF == 
   13.15   *---------------------------------------------------------------------------*)
   13.16 -val rew::prems = goal thy
   13.17 +val rew::prems = goal (the_context ())
   13.18      "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
   13.19  by (rewtac rew);
   13.20  by (REPEAT (resolve_tac (prems@[wfrec]) 1));
    14.1 --- a/src/HOL/WF_Rel.ML	Mon Jul 24 23:51:11 2000 +0200
    14.2 +++ b/src/HOL/WF_Rel.ML	Mon Jul 24 23:51:46 2000 +0200
    14.3 @@ -72,7 +72,7 @@
    14.4   * Wellfoundedness of lexicographic combinations
    14.5   *---------------------------------------------------------------------------*)
    14.6  
    14.7 -val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
    14.8 +val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
    14.9   "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
   14.10  by (EVERY1 [rtac allI,rtac impI]);
   14.11  by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
    15.1 --- a/src/HOL/equalities.ML	Mon Jul 24 23:51:11 2000 +0200
    15.2 +++ b/src/HOL/equalities.ML	Mon Jul 24 23:51:46 2000 +0200
    15.3 @@ -104,7 +104,7 @@
    15.4  by (Blast_tac 1);
    15.5  qed "mk_disjoint_insert";
    15.6  
    15.7 -bind_thm ("insert_Collect", prove_goal thy 
    15.8 +bind_thm ("insert_Collect", prove_goal (the_context ())
    15.9  	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
   15.10  
   15.11  Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
   15.12 @@ -900,7 +900,7 @@
   15.13  
   15.14  (** Miniscoping: pushing in big Unions and Intersections **)
   15.15  local
   15.16 -  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
   15.17 +  fun prover s = prove_goal (the_context ()) s (fn _ => [Blast_tac 1])
   15.18  in
   15.19  val UN_simps = map prover 
   15.20      ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",