uniform Proof.context for hyp_subst_tac;
authorwenzelm
Sat Apr 27 20:50:20 2013 +0200 (2013-04-27 ago)
changeset 51798ad3a241def73
parent 51797 182454c06a80
child 51799 8fcf6e32544e
uniform Proof.context for hyp_subst_tac;
src/CCL/Wfd.thy
src/Doc/ZF/IFOL_examples.thy
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOL/ex/Intuitionistic.thy
src/FOL/ex/Propositional_Cla.thy
src/FOL/ex/Propositional_Int.thy
src/FOL/ex/Quantifiers_Int.thy
src/FOL/intprover.ML
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/Bali/AxSem.thy
src/HOL/HOL.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Purchase.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Pure/Isar/context_rules.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/CCL/Wfd.thy	Sat Apr 27 11:37:50 2013 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Sat Apr 27 20:50:20 2013 +0200
     1.3 @@ -473,14 +473,11 @@
     1.4  
     1.5  (*** Clean up Correctness Condictions ***)
     1.6  
     1.7 -val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
     1.8 -                                 hyp_subst_tac)
     1.9 -
    1.10  fun clean_ccs_tac ctxt =
    1.11    let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
    1.12      TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
    1.13 -    eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    1.14 -    hyp_subst_tac))
    1.15 +      eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    1.16 +      hyp_subst_tac ctxt))
    1.17    end
    1.18  
    1.19  fun gen_ccs_tac ctxt rls i =
     2.1 --- a/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 11:37:50 2013 +0200
     2.2 +++ b/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 20:50:20 2013 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4  done
     2.5  
     2.6  lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
     2.7 -by (tactic {*IntPr.fast_tac 1*})
     2.8 +by (tactic {*IntPr.fast_tac @{context} 1*})
     2.9  
    2.10  text{*Example of Dyckhoff's method*}
    2.11  lemma "~ ~ ((P-->Q) | (Q-->P))"
     3.1 --- a/src/FOL/FOL.thy	Sat Apr 27 11:37:50 2013 +0200
     3.2 +++ b/src/FOL/FOL.thy	Sat Apr 27 20:50:20 2013 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4    proof (rule r)
     3.5      { fix y y'
     3.6        assume "P(y)" and "P(y')"
     3.7 -      with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+
     3.8 +      with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
     3.9        then have "y = y'" by (rule subst)
    3.10      } note r' = this
    3.11      show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
     4.1 --- a/src/FOL/IFOL.thy	Sat Apr 27 11:37:50 2013 +0200
     4.2 +++ b/src/FOL/IFOL.thy	Sat Apr 27 20:50:20 2013 +0200
     4.3 @@ -635,7 +635,7 @@
     4.4    and [Pure.elim 2] = allE notE' impE'
     4.5    and [Pure.intro] = exI disjI2 disjI1
     4.6  
     4.7 -setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
     4.8 +setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *}
     4.9  
    4.10  
    4.11  lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
     5.1 --- a/src/FOL/ex/Intuitionistic.thy	Sat Apr 27 11:37:50 2013 +0200
     5.2 +++ b/src/FOL/ex/Intuitionistic.thy	Sat Apr 27 20:50:20 2013 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  by (assume_tac 1);
     5.5  by (IntPr.safe_tac 1);
     5.6  by (IntPr.mp_tac 1);
     5.7 -by (IntPr.fast_tac 1);
     5.8 +by (IntPr.fast_tac @{context} 1);
     5.9  *)
    5.10  
    5.11  
    5.12 @@ -37,55 +37,55 @@
    5.13  is intuitionstically equivalent to $P$.  [Andy Pitts] *}
    5.14  
    5.15  lemma "~~(P&Q) <-> ~~P & ~~Q"
    5.16 -by (tactic{*IntPr.fast_tac 1*})
    5.17 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.18  
    5.19  lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
    5.20 -by (tactic{*IntPr.fast_tac 1*})
    5.21 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.22  
    5.23  text{*Double-negation does NOT distribute over disjunction*}
    5.24  
    5.25  lemma "~~(P-->Q)  <-> (~~P --> ~~Q)"
    5.26 -by (tactic{*IntPr.fast_tac 1*})
    5.27 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.28  
    5.29  lemma "~~~P <-> ~P"
    5.30 -by (tactic{*IntPr.fast_tac 1*})
    5.31 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.32  
    5.33  lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
    5.34 -by (tactic{*IntPr.fast_tac 1*})
    5.35 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.36  
    5.37  lemma "(P<->Q) <-> (Q<->P)"
    5.38 -by (tactic{*IntPr.fast_tac 1*})
    5.39 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.40  
    5.41  lemma "((P --> (Q | (Q-->R))) --> R) --> R"
    5.42 -by (tactic{*IntPr.fast_tac 1*})
    5.43 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.44  
    5.45  lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
    5.46        --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
    5.47        --> (((F-->A)-->B) --> I) --> E"
    5.48 -by (tactic{*IntPr.fast_tac 1*})
    5.49 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.50  
    5.51  
    5.52  text{*Lemmas for the propositional double-negation translation*}
    5.53  
    5.54  lemma "P --> ~~P"
    5.55 -by (tactic{*IntPr.fast_tac 1*})
    5.56 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.57  
    5.58  lemma "~~(~~P --> P)"
    5.59 -by (tactic{*IntPr.fast_tac 1*})
    5.60 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.61  
    5.62  lemma "~~P & ~~(P --> Q) --> ~~Q"
    5.63 -by (tactic{*IntPr.fast_tac 1*})
    5.64 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.65  
    5.66  
    5.67  text{*The following are classically but not constructively valid.
    5.68        The attempt to prove them terminates quickly!*}
    5.69  lemma "((P-->Q) --> P)  -->  P"
    5.70 -apply (tactic{*IntPr.fast_tac 1*} | -)
    5.71 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
    5.72  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
    5.73  oops
    5.74  
    5.75  lemma "(P&Q-->R)  -->  (P-->R) | (Q-->R)"
    5.76 -apply (tactic{*IntPr.fast_tac 1*} | -)
    5.77 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
    5.78  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
    5.79  oops
    5.80  
    5.81 @@ -96,7 +96,7 @@
    5.82  lemma "((P<->Q) --> P&Q&R) &
    5.83                 ((Q<->R) --> P&Q&R) &
    5.84                 ((R<->P) --> P&Q&R) --> P&Q&R"
    5.85 -by (tactic{*IntPr.fast_tac 1*})
    5.86 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.87  
    5.88  
    5.89  text{*de Bruijn formula with five predicates*}
    5.90 @@ -105,7 +105,7 @@
    5.91                 ((R<->S) --> P&Q&R&S&T) &
    5.92                 ((S<->T) --> P&Q&R&S&T) &
    5.93                 ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T"
    5.94 -by (tactic{*IntPr.fast_tac 1*})
    5.95 +by (tactic{*IntPr.fast_tac @{context} 1*})
    5.96  
    5.97  
    5.98  (*** Problems from of Sahlin, Franzen and Haridi,
    5.99 @@ -116,11 +116,11 @@
   5.100  text{*Problem 1.1*}
   5.101  lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->
   5.102        (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
   5.103 -by (tactic{*IntPr.best_dup_tac 1*})  --{*SLOW*}
   5.104 +by (tactic{*IntPr.best_dup_tac @{context} 1*})  --{*SLOW*}
   5.105  
   5.106  text{*Problem 3.1*}
   5.107  lemma "~ (EX x. ALL y. mem(y,x) <-> ~ mem(x,x))"
   5.108 -by (tactic{*IntPr.fast_tac 1*})
   5.109 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.110  
   5.111  text{*Problem 4.1: hopeless!*}
   5.112  lemma "(ALL x. p(x) --> p(h(x)) | p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))
   5.113 @@ -132,78 +132,78 @@
   5.114  
   5.115  text{*~~1*}
   5.116  lemma "~~((P-->Q)  <->  (~Q --> ~P))"
   5.117 -by (tactic{*IntPr.fast_tac 1*})
   5.118 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.119  
   5.120  text{*~~2*}
   5.121  lemma "~~(~~P  <->  P)"
   5.122 -by (tactic{*IntPr.fast_tac 1*})
   5.123 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.124  
   5.125  text{*3*}
   5.126  lemma "~(P-->Q) --> (Q-->P)"
   5.127 -by (tactic{*IntPr.fast_tac 1*})
   5.128 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.129  
   5.130  text{*~~4*}
   5.131  lemma "~~((~P-->Q)  <->  (~Q --> P))"
   5.132 -by (tactic{*IntPr.fast_tac 1*})
   5.133 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.134  
   5.135  text{*~~5*}
   5.136  lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
   5.137 -by (tactic{*IntPr.fast_tac 1*})
   5.138 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.139  
   5.140  text{*~~6*}
   5.141  lemma "~~(P | ~P)"
   5.142 -by (tactic{*IntPr.fast_tac 1*})
   5.143 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.144  
   5.145  text{*~~7*}
   5.146  lemma "~~(P | ~~~P)"
   5.147 -by (tactic{*IntPr.fast_tac 1*})
   5.148 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.149  
   5.150  text{*~~8.  Peirce's law*}
   5.151  lemma "~~(((P-->Q) --> P)  -->  P)"
   5.152 -by (tactic{*IntPr.fast_tac 1*})
   5.153 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.154  
   5.155  text{*9*}
   5.156  lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   5.157 -by (tactic{*IntPr.fast_tac 1*})
   5.158 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.159  
   5.160  text{*10*}
   5.161  lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
   5.162 -by (tactic{*IntPr.fast_tac 1*})
   5.163 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.164  
   5.165  subsection{*11.  Proved in each direction (incorrectly, says Pelletier!!) *}
   5.166  lemma "P<->P"
   5.167 -by (tactic{*IntPr.fast_tac 1*})
   5.168 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.169  
   5.170  text{*~~12.  Dijkstra's law  *}
   5.171  lemma "~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
   5.172 -by (tactic{*IntPr.fast_tac 1*})
   5.173 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.174  
   5.175  lemma "((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
   5.176 -by (tactic{*IntPr.fast_tac 1*})
   5.177 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.178  
   5.179  text{*13.  Distributive law*}
   5.180  lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
   5.181 -by (tactic{*IntPr.fast_tac 1*})
   5.182 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.183  
   5.184  text{*~~14*}
   5.185  lemma "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
   5.186 -by (tactic{*IntPr.fast_tac 1*})
   5.187 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.188  
   5.189  text{*~~15*}
   5.190  lemma "~~((P --> Q) <-> (~P | Q))"
   5.191 -by (tactic{*IntPr.fast_tac 1*})
   5.192 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.193  
   5.194  text{*~~16*}
   5.195  lemma "~~((P-->Q) | (Q-->P))"
   5.196 -by (tactic{*IntPr.fast_tac 1*})
   5.197 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.198  
   5.199  text{*~~17*}
   5.200  lemma "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
   5.201 -by (tactic{*IntPr.fast_tac 1*})
   5.202 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.203  
   5.204  text{*Dijkstra's "Golden Rule"*}
   5.205  lemma "(P&Q) <-> P <-> Q <-> (P|Q)"
   5.206 -by (tactic{*IntPr.fast_tac 1*})
   5.207 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.208  
   5.209  
   5.210  subsection{*****Examples with quantifiers*****}
   5.211 @@ -212,19 +212,19 @@
   5.212  subsection{*The converse is classical in the following implications...*}
   5.213  
   5.214  lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
   5.215 -by (tactic{*IntPr.fast_tac 1*})
   5.216 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.217  
   5.218  lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
   5.219 -by (tactic{*IntPr.fast_tac 1*})
   5.220 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.221  
   5.222  lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
   5.223 -by (tactic{*IntPr.fast_tac 1*})
   5.224 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.225  
   5.226  lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
   5.227 -by (tactic{*IntPr.fast_tac 1*})
   5.228 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.229  
   5.230  lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
   5.231 -by (tactic{*IntPr.fast_tac 1*})
   5.232 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.233  
   5.234  
   5.235  
   5.236 @@ -233,28 +233,28 @@
   5.237  text{*The attempt to prove them terminates quickly!*}
   5.238  
   5.239  lemma "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
   5.240 -apply (tactic{*IntPr.fast_tac 1*} | -)
   5.241 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
   5.242  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
   5.243  oops
   5.244  
   5.245  lemma "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
   5.246 -apply (tactic{*IntPr.fast_tac 1*} | -)
   5.247 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
   5.248  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
   5.249  oops
   5.250  
   5.251  lemma "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
   5.252 -apply (tactic{*IntPr.fast_tac 1*} | -)
   5.253 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
   5.254  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
   5.255  oops
   5.256  
   5.257  lemma "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
   5.258 -apply (tactic{*IntPr.fast_tac 1*} | -)
   5.259 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
   5.260  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
   5.261  oops
   5.262  
   5.263  text{*Classically but not intuitionistically valid.  Proved by a bug in 1986!*}
   5.264  lemma "EX x. Q(x) --> (ALL x. Q(x))"
   5.265 -apply (tactic{*IntPr.fast_tac 1*} | -)
   5.266 +apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
   5.267  apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
   5.268  oops
   5.269  
   5.270 @@ -275,7 +275,7 @@
   5.271  text{*20*}
   5.272  lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
   5.273      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
   5.274 -by (tactic{*IntPr.fast_tac 1*})
   5.275 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.276  
   5.277  text{*21*}
   5.278  lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"
   5.279 @@ -283,11 +283,11 @@
   5.280  
   5.281  text{*22*}
   5.282  lemma "(ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
   5.283 -by (tactic{*IntPr.fast_tac 1*})
   5.284 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.285  
   5.286  text{*~~23*}
   5.287  lemma "~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
   5.288 -by (tactic{*IntPr.fast_tac 1*})
   5.289 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.290  
   5.291  text{*24*}
   5.292  lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
   5.293 @@ -295,10 +295,10 @@
   5.294      --> ~~(EX x. P(x)&R(x))"
   5.295  txt{*Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and 
   5.296      @{text ITER_DEEPEN} all take forever*}
   5.297 -apply (tactic{* IntPr.safe_tac*})
   5.298 +apply (tactic{* IntPr.safe_tac @{context}*})
   5.299  apply (erule impE)
   5.300 -apply (tactic{*IntPr.fast_tac 1*})
   5.301 -by (tactic{*IntPr.fast_tac 1*})
   5.302 +apply (tactic{*IntPr.fast_tac @{context} 1*})
   5.303 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.304  
   5.305  text{*25*}
   5.306  lemma "(EX x. P(x)) &
   5.307 @@ -306,7 +306,7 @@
   5.308          (ALL x. P(x) --> (M(x) & L(x))) &
   5.309          ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
   5.310      --> (EX x. Q(x)&P(x))"
   5.311 -by (tactic{*IntPr.fast_tac 1*})
   5.312 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.313  
   5.314  text{*~~26*}
   5.315  lemma "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &
   5.316 @@ -320,45 +320,45 @@
   5.317                (ALL x. M(x) & L(x) --> P(x)) &
   5.318                ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
   5.319            --> (ALL x. M(x) --> ~L(x))"
   5.320 -by (tactic{*IntPr.fast_tac 1*})
   5.321 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.322  
   5.323  text{*~~28.  AMENDED*}
   5.324  lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
   5.325          (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
   5.326          (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
   5.327      --> (ALL x. P(x) & L(x) --> M(x))"
   5.328 -by (tactic{*IntPr.fast_tac 1*})
   5.329 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.330  
   5.331  text{*29.  Essentially the same as Principia Mathematica *11.71*}
   5.332  lemma "(EX x. P(x)) & (EX y. Q(y))
   5.333      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->
   5.334           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
   5.335 -by (tactic{*IntPr.fast_tac 1*})
   5.336 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.337  
   5.338  text{*~~30*}
   5.339  lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
   5.340          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
   5.341      --> (ALL x. ~~S(x))"
   5.342 -by (tactic{*IntPr.fast_tac 1*})
   5.343 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.344  
   5.345  text{*31*}
   5.346  lemma "~(EX x. P(x) & (Q(x) | R(x))) &
   5.347          (EX x. L(x) & P(x)) &
   5.348          (ALL x. ~ R(x) --> M(x))
   5.349      --> (EX x. L(x) & M(x))"
   5.350 -by (tactic{*IntPr.fast_tac 1*})
   5.351 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.352  
   5.353  text{*32*}
   5.354  lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
   5.355          (ALL x. S(x) & R(x) --> L(x)) &
   5.356          (ALL x. M(x) --> R(x))
   5.357      --> (ALL x. P(x) & M(x) --> L(x))"
   5.358 -by (tactic{*IntPr.fast_tac 1*})
   5.359 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.360  
   5.361  text{*~~33*}
   5.362  lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  <->
   5.363        (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
   5.364 -apply (tactic{*IntPr.best_tac 1*})
   5.365 +apply (tactic{*IntPr.best_tac @{context} 1*})
   5.366  done
   5.367  
   5.368  
   5.369 @@ -367,7 +367,7 @@
   5.370        (ALL x. EX y. G(x,y)) &
   5.371        (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
   5.372    --> (ALL x. EX y. H(x,y))"
   5.373 -by (tactic{*IntPr.fast_tac 1*})
   5.374 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.375  
   5.376  text{*37*}
   5.377  lemma "(ALL z. EX w. ALL x. EX y.
   5.378 @@ -379,47 +379,47 @@
   5.379  
   5.380  text{*39*}
   5.381  lemma "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   5.382 -by (tactic{*IntPr.fast_tac 1*})
   5.383 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.384  
   5.385  text{*40.  AMENDED*}
   5.386  lemma "(EX y. ALL x. F(x,y) <-> F(x,x)) -->
   5.387                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
   5.388 -by (tactic{*IntPr.fast_tac 1*})
   5.389 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.390  
   5.391  text{*44*}
   5.392  lemma "(ALL x. f(x) -->
   5.393                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &
   5.394                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
   5.395                --> (EX x. j(x) & ~f(x))"
   5.396 -by (tactic{*IntPr.fast_tac 1*})
   5.397 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.398  
   5.399  text{*48*}
   5.400  lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   5.401 -by (tactic{*IntPr.fast_tac 1*})
   5.402 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.403  
   5.404  text{*51*}
   5.405  lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
   5.406       (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
   5.407 -by (tactic{*IntPr.fast_tac 1*})
   5.408 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.409  
   5.410  text{*52*}
   5.411  text{*Almost the same as 51. *}
   5.412  lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
   5.413       (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
   5.414 -by (tactic{*IntPr.fast_tac 1*})
   5.415 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.416  
   5.417  text{*56*}
   5.418  lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   5.419 -by (tactic{*IntPr.fast_tac 1*})
   5.420 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.421  
   5.422  text{*57*}
   5.423  lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
   5.424       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   5.425 -by (tactic{*IntPr.fast_tac 1*})
   5.426 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.427  
   5.428  text{*60*}
   5.429  lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   5.430 -by (tactic{*IntPr.fast_tac 1*})
   5.431 +by (tactic{*IntPr.fast_tac @{context} 1*})
   5.432  
   5.433  end
   5.434  
     6.1 --- a/src/FOL/ex/Propositional_Cla.thy	Sat Apr 27 11:37:50 2013 +0200
     6.2 +++ b/src/FOL/ex/Propositional_Cla.thy	Sat Apr 27 20:50:20 2013 +0200
     6.3 @@ -12,7 +12,7 @@
     6.4  text {* commutative laws of @{text "&"} and @{text "|"} *}
     6.5  
     6.6  lemma "P & Q  -->  Q & P"
     6.7 -  by (tactic "IntPr.fast_tac 1")
     6.8 +  by (tactic "IntPr.fast_tac @{context} 1")
     6.9  
    6.10  lemma "P | Q  -->  Q | P"
    6.11    by fast
     7.1 --- a/src/FOL/ex/Propositional_Int.thy	Sat Apr 27 11:37:50 2013 +0200
     7.2 +++ b/src/FOL/ex/Propositional_Int.thy	Sat Apr 27 20:50:20 2013 +0200
     7.3 @@ -12,106 +12,106 @@
     7.4  text {* commutative laws of @{text "&"} and @{text "|"} *}
     7.5  
     7.6  lemma "P & Q  -->  Q & P"
     7.7 -  by (tactic "IntPr.fast_tac 1")
     7.8 +  by (tactic "IntPr.fast_tac @{context} 1")
     7.9  
    7.10  lemma "P | Q  -->  Q | P"
    7.11 -  by (tactic "IntPr.fast_tac 1")
    7.12 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.13  
    7.14  
    7.15  text {* associative laws of @{text "&"} and @{text "|"} *}
    7.16  lemma "(P & Q) & R  -->  P & (Q & R)"
    7.17 -  by (tactic "IntPr.fast_tac 1")
    7.18 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.19  
    7.20  lemma "(P | Q) | R  -->  P | (Q | R)"
    7.21 -  by (tactic "IntPr.fast_tac 1")
    7.22 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.23  
    7.24  
    7.25  text {* distributive laws of @{text "&"} and @{text "|"} *}
    7.26  lemma "(P & Q) | R  --> (P | R) & (Q | R)"
    7.27 -  by (tactic "IntPr.fast_tac 1")
    7.28 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.29  
    7.30  lemma "(P | R) & (Q | R)  --> (P & Q) | R"
    7.31 -  by (tactic "IntPr.fast_tac 1")
    7.32 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.33  
    7.34  lemma "(P | Q) & R  --> (P & R) | (Q & R)"
    7.35 -  by (tactic "IntPr.fast_tac 1")
    7.36 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.37  
    7.38  lemma "(P & R) | (Q & R)  --> (P | Q) & R"
    7.39 -  by (tactic "IntPr.fast_tac 1")
    7.40 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.41  
    7.42  
    7.43  text {* Laws involving implication *}
    7.44  
    7.45  lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
    7.46 -  by (tactic "IntPr.fast_tac 1")
    7.47 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.48  
    7.49  lemma "(P & Q --> R) <-> (P--> (Q-->R))"
    7.50 -  by (tactic "IntPr.fast_tac 1")
    7.51 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.52  
    7.53  lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
    7.54 -  by (tactic "IntPr.fast_tac 1")
    7.55 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.56  
    7.57  lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
    7.58 -  by (tactic "IntPr.fast_tac 1")
    7.59 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.60  
    7.61  lemma "(P --> Q & R) <-> (P-->Q)  &  (P-->R)"
    7.62 -  by (tactic "IntPr.fast_tac 1")
    7.63 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.64  
    7.65  
    7.66  text {* Propositions-as-types *}
    7.67  
    7.68  -- {* The combinator K *}
    7.69  lemma "P --> (Q --> P)"
    7.70 -  by (tactic "IntPr.fast_tac 1")
    7.71 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.72  
    7.73  -- {* The combinator S *}
    7.74  lemma "(P-->Q-->R)  --> (P-->Q) --> (P-->R)"
    7.75 -  by (tactic "IntPr.fast_tac 1")
    7.76 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.77  
    7.78  
    7.79  -- {* Converse is classical *}
    7.80  lemma "(P-->Q) | (P-->R)  -->  (P --> Q | R)"
    7.81 -  by (tactic "IntPr.fast_tac 1")
    7.82 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.83  
    7.84  lemma "(P-->Q)  -->  (~Q --> ~P)"
    7.85 -  by (tactic "IntPr.fast_tac 1")
    7.86 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.87  
    7.88  
    7.89  text {* Schwichtenberg's examples (via T. Nipkow) *}
    7.90  
    7.91  lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
    7.92 -  by (tactic "IntPr.fast_tac 1")
    7.93 +  by (tactic "IntPr.fast_tac @{context} 1")
    7.94  
    7.95  lemma stab_to_peirce:
    7.96    "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
    7.97                                --> ((P --> Q) --> P) --> P"
    7.98 -  by (tactic "IntPr.fast_tac 1")
    7.99 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.100  
   7.101  lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)  
   7.102                  --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
   7.103 -  by (tactic "IntPr.fast_tac 1")
   7.104 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.105    
   7.106  lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
   7.107 -  by (tactic "IntPr.fast_tac 1")
   7.108 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.109  
   7.110  lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
   7.111 -  by (tactic "IntPr.fast_tac 1")
   7.112 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.113  
   7.114  lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
   7.115 -  by (tactic "IntPr.fast_tac 1")
   7.116 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.117  
   7.118  lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)  
   7.119    --> (((P8 --> P2) --> P9) --> P3 --> P10)  
   7.120    --> (P1 --> P8) --> P6 --> P7  
   7.121    --> (((P3 --> P2) --> P9) --> P4)  
   7.122    --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
   7.123 -  by (tactic "IntPr.fast_tac 1")
   7.124 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.125  
   7.126  lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)  
   7.127    --> (((P3 --> P2) --> P9) --> P4)  
   7.128    --> (((P6 --> P1) --> P2) --> P9)  
   7.129    --> (((P7 --> P1) --> P10) --> P4 --> P5)  
   7.130    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
   7.131 -  by (tactic "IntPr.fast_tac 1")
   7.132 +  by (tactic "IntPr.fast_tac @{context} 1")
   7.133  
   7.134  end
     8.1 --- a/src/FOL/ex/Quantifiers_Int.thy	Sat Apr 27 11:37:50 2013 +0200
     8.2 +++ b/src/FOL/ex/Quantifiers_Int.thy	Sat Apr 27 20:50:20 2013 +0200
     8.3 @@ -10,91 +10,91 @@
     8.4  begin
     8.5  
     8.6  lemma "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
     8.7 -  by (tactic "IntPr.fast_tac 1")
     8.8 +  by (tactic "IntPr.fast_tac @{context} 1")
     8.9  
    8.10  lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
    8.11 -  by (tactic "IntPr.fast_tac 1")
    8.12 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.13  
    8.14  
    8.15  -- {* Converse is false *}
    8.16  lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
    8.17 -  by (tactic "IntPr.fast_tac 1")
    8.18 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.19  
    8.20  lemma "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
    8.21 -  by (tactic "IntPr.fast_tac 1")
    8.22 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.23  
    8.24  
    8.25  lemma "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
    8.26 -  by (tactic "IntPr.fast_tac 1")
    8.27 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.28  
    8.29  
    8.30  text {* Some harder ones *}
    8.31  
    8.32  lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
    8.33 -  by (tactic "IntPr.fast_tac 1")
    8.34 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.35  
    8.36  -- {* Converse is false *}
    8.37  lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
    8.38 -  by (tactic "IntPr.fast_tac 1")
    8.39 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.40  
    8.41  
    8.42  text {* Basic test of quantifier reasoning *}
    8.43  
    8.44  -- {* TRUE *}
    8.45  lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    8.46 -  by (tactic "IntPr.fast_tac 1")
    8.47 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.48  
    8.49  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    8.50 -  by (tactic "IntPr.fast_tac 1")
    8.51 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.52  
    8.53  
    8.54  text {* The following should fail, as they are false! *}
    8.55  
    8.56  lemma "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
    8.57 -  apply (tactic "IntPr.fast_tac 1")?
    8.58 +  apply (tactic "IntPr.fast_tac @{context} 1")?
    8.59    oops
    8.60  
    8.61  lemma "(EX x. Q(x))  -->  (ALL x. Q(x))"
    8.62 -  apply (tactic "IntPr.fast_tac 1")?
    8.63 +  apply (tactic "IntPr.fast_tac @{context} 1")?
    8.64    oops
    8.65  
    8.66  schematic_lemma "P(?a) --> (ALL x. P(x))"
    8.67 -  apply (tactic "IntPr.fast_tac 1")?
    8.68 +  apply (tactic "IntPr.fast_tac @{context} 1")?
    8.69    oops
    8.70  
    8.71  schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
    8.72 -  apply (tactic "IntPr.fast_tac 1")?
    8.73 +  apply (tactic "IntPr.fast_tac @{context} 1")?
    8.74    oops
    8.75  
    8.76  
    8.77  text {* Back to things that are provable \dots *}
    8.78  
    8.79  lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
    8.80 -  by (tactic "IntPr.fast_tac 1")
    8.81 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.82  
    8.83  -- {* An example of why exI should be delayed as long as possible *}
    8.84  lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
    8.85 -  by (tactic "IntPr.fast_tac 1")
    8.86 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.87  
    8.88  schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
    8.89 -  by (tactic "IntPr.fast_tac 1")
    8.90 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.91  
    8.92  lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    8.93 -  by (tactic "IntPr.fast_tac 1")
    8.94 +  by (tactic "IntPr.fast_tac @{context} 1")
    8.95  
    8.96  
    8.97  text {* Some slow ones *}
    8.98  
    8.99  -- {* Principia Mathematica *11.53 *}
   8.100  lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
   8.101 -  by (tactic "IntPr.fast_tac 1")
   8.102 +  by (tactic "IntPr.fast_tac @{context} 1")
   8.103  
   8.104  (*Principia Mathematica *11.55  *)
   8.105  lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
   8.106 -  by (tactic "IntPr.fast_tac 1")
   8.107 +  by (tactic "IntPr.fast_tac @{context} 1")
   8.108  
   8.109  (*Principia Mathematica *11.61  *)
   8.110  lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
   8.111 -  by (tactic "IntPr.fast_tac 1")
   8.112 +  by (tactic "IntPr.fast_tac @{context} 1")
   8.113  
   8.114  end
     9.1 --- a/src/FOL/intprover.ML	Sat Apr 27 11:37:50 2013 +0200
     9.2 +++ b/src/FOL/intprover.ML	Sat Apr 27 20:50:20 2013 +0200
     9.3 @@ -16,19 +16,19 @@
     9.4  *)
     9.5  
     9.6  signature INT_PROVER = 
     9.7 -  sig
     9.8 -  val best_tac: int -> tactic
     9.9 -  val best_dup_tac: int -> tactic
    9.10 -  val fast_tac: int -> tactic
    9.11 +sig
    9.12 +  val best_tac: Proof.context -> int -> tactic
    9.13 +  val best_dup_tac: Proof.context -> int -> tactic
    9.14 +  val fast_tac: Proof.context -> int -> tactic
    9.15    val inst_step_tac: int -> tactic
    9.16 -  val safe_step_tac: int -> tactic
    9.17 +  val safe_step_tac: Proof.context -> int -> tactic
    9.18    val safe_brls: (bool * thm) list
    9.19 -  val safe_tac: tactic
    9.20 -  val step_tac: int -> tactic
    9.21 -  val step_dup_tac: int -> tactic
    9.22 +  val safe_tac: Proof.context -> tactic
    9.23 +  val step_tac: Proof.context -> int -> tactic
    9.24 +  val step_dup_tac: Proof.context -> int -> tactic
    9.25    val haz_brls: (bool * thm) list
    9.26    val haz_dup_brls: (bool * thm) list
    9.27 -  end;
    9.28 +end;
    9.29  
    9.30  
    9.31  structure IntPr : INT_PROVER   = 
    9.32 @@ -62,14 +62,16 @@
    9.33      List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
    9.34  
    9.35  (*Attack subgoals using safe inferences -- matching, not resolution*)
    9.36 -val safe_step_tac = FIRST' [eq_assume_tac,
    9.37 -                            eq_mp_tac,
    9.38 -                            bimatch_tac safe0_brls,
    9.39 -                            hyp_subst_tac,
    9.40 -                            bimatch_tac safep_brls] ;
    9.41 +fun safe_step_tac ctxt =
    9.42 +  FIRST' [
    9.43 +    eq_assume_tac,
    9.44 +    eq_mp_tac,
    9.45 +    bimatch_tac safe0_brls,
    9.46 +    hyp_subst_tac ctxt,
    9.47 +    bimatch_tac safep_brls];
    9.48  
    9.49  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
    9.50 -val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
    9.51 +fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
    9.52  
    9.53  (*These steps could instantiate variables and are therefore unsafe.*)
    9.54  val inst_step_tac =
    9.55 @@ -77,20 +79,20 @@
    9.56    biresolve_tac (safe0_brls @ safep_brls);
    9.57  
    9.58  (*One safe or unsafe step. *)
    9.59 -fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
    9.60 +fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i];
    9.61  
    9.62 -fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
    9.63 +fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i];
    9.64  
    9.65  (*Dumb but fast*)
    9.66 -val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
    9.67 +fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
    9.68  
    9.69  (*Slower but smarter than fast_tac*)
    9.70 -val best_tac = 
    9.71 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
    9.72 +fun best_tac ctxt =
    9.73 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
    9.74  
    9.75  (*Uses all_dupE: allows multiple use of universal assumptions.  VERY slow.*)
    9.76 -val best_dup_tac = 
    9.77 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1));
    9.78 +fun best_dup_tac ctxt =
    9.79 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
    9.80  
    9.81  
    9.82  end;
    10.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 11:37:50 2013 +0200
    10.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 20:50:20 2013 +0200
    10.3 @@ -258,9 +258,9 @@
    10.4  
    10.5  method_setup disentangle = {*
    10.6      Scan.succeed
    10.7 -     (K (SIMPLE_METHOD
    10.8 +     (fn ctxt => SIMPLE_METHOD
    10.9        (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
   10.10 -                   ORELSE' hyp_subst_tac)))) *}
   10.11 +                   ORELSE' hyp_subst_tac ctxt))) *}
   10.12    "for eliminating conjunctions, disjunctions and the like"
   10.13  
   10.14  
    11.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Apr 27 11:37:50 2013 +0200
    11.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Apr 27 20:50:20 2013 +0200
    11.3 @@ -751,11 +751,11 @@
    11.4   (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
    11.5   (*Base*)  (force_tac ctxt) 1
    11.6  
    11.7 -val analz_prepare_tac = 
    11.8 +fun analz_prepare_tac ctxt =
    11.9           prepare_tac THEN
   11.10           dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN 
   11.11   (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN 
   11.12 -         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
   11.13 +         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
   11.14  
   11.15  end
   11.16  *}
   11.17 @@ -769,7 +769,7 @@
   11.18    "additional facts to reason about parts"
   11.19  
   11.20  method_setup analz_prepare = {*
   11.21 -    Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
   11.22 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.analz_prepare_tac ctxt)) *}
   11.23    "additional facts to reason about analz"
   11.24  
   11.25  
    12.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Apr 27 11:37:50 2013 +0200
    12.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Apr 27 20:50:20 2013 +0200
    12.3 @@ -764,7 +764,7 @@
    12.4           prepare_tac ctxt THEN
    12.5           dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
    12.6   (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
    12.7 -         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
    12.8 +         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
    12.9  
   12.10  end
   12.11  *}
    13.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    13.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    13.3 @@ -221,7 +221,7 @@
    13.4      REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
    13.5      (TRY o dresolve_tac Gwit_thms THEN'
    13.6      (etac FalseE ORELSE'
    13.7 -    hyp_subst_tac THEN'
    13.8 +    hyp_subst_tac ctxt THEN'
    13.9      dresolve_tac Fwit_thms THEN'
   13.10      (etac FalseE ORELSE' atac))) 1);
   13.11  
    14.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sat Apr 27 11:37:50 2013 +0200
    14.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sat Apr 27 20:50:20 2013 +0200
    14.3 @@ -504,7 +504,7 @@
    14.4                    val half_goalss = map mk_goal half_pairss;
    14.5                    val half_thmss =
    14.6                      map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
    14.7 -                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
    14.8 +                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
    14.9                        half_goalss half_pairss (flat disc_thmss');
   14.10  
   14.11                    val other_half_goalss = map (mk_goal o map swap) half_pairss;
    15.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    15.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    15.3 @@ -15,7 +15,7 @@
    15.4    val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    15.5    val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    15.6      thm list list list -> thm list list list -> tactic
    15.7 -  val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
    15.8 +  val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
    15.9    val mk_nchotomy_tac: int -> thm -> tactic
   15.10    val mk_other_half_disc_exclude_tac: thm -> tactic
   15.11    val mk_split_tac: Proof.context ->
   15.12 @@ -44,13 +44,13 @@
   15.13  fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
   15.14    EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
   15.15      rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
   15.16 -    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
   15.17 +    hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
   15.18      rtac distinct, rtac uexhaust] @
   15.19      (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
   15.20       |> k = 1 ? swap |> op @)) 1;
   15.21  
   15.22 -fun mk_half_disc_exclude_tac m discD disc' =
   15.23 -  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
   15.24 +fun mk_half_disc_exclude_tac ctxt m discD disc' =
   15.25 +  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' rtac disc') 1;
   15.26  
   15.27  fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
   15.28  
   15.29 @@ -64,7 +64,7 @@
   15.30     (if m = 0 then
   15.31        atac
   15.32      else
   15.33 -      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
   15.34 +      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
   15.35        SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
   15.36  
   15.37  fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
   15.38 @@ -100,7 +100,7 @@
   15.39  fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
   15.40    (rtac uexhaust THEN'
   15.41     EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   15.42 -       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
   15.43 +       EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
   15.44       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
   15.45  
   15.46  fun mk_case_cong_tac ctxt uexhaust cases =
   15.47 @@ -112,7 +112,7 @@
   15.48  (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
   15.49  fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   15.50    rtac uexhaust 1 THEN
   15.51 -  ALLGOALS (fn k => (hyp_subst_tac THEN'
   15.52 +  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
   15.53       simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
   15.54         flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   15.55    ALLGOALS (blast_tac naked_ctxt);
    16.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sat Apr 27 11:37:50 2013 +0200
    16.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat Apr 27 20:50:20 2013 +0200
    16.3 @@ -971,7 +971,8 @@
    16.4                  (Logic.list_implies (prems_cong,
    16.5                    mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
    16.6            in
    16.7 -            Goal.prove_sorry lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
    16.8 +            Goal.prove_sorry lthy [] [] in_cong_goal
    16.9 +              (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1))
   16.10              |> Thm.close_derivation
   16.11            end;
   16.12  
   16.13 @@ -989,7 +990,7 @@
   16.14              val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
   16.15                (Logic.list_implies (prem0 :: prems, eq));
   16.16            in
   16.17 -            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac (#map_cong0 axioms))
   16.18 +            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
   16.19              |> Thm.close_derivation
   16.20            end;
   16.21  
   16.22 @@ -1073,7 +1074,7 @@
   16.23            in
   16.24              Goal.prove_sorry lthy [] []
   16.25                (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
   16.26 -              (fn _ => (TRY o hyp_subst_tac THEN' rtac refl) 1)
   16.27 +              (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1)
   16.28              |> Thm.close_derivation
   16.29            end;
   16.30  
    17.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    17.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    17.3 @@ -11,7 +11,7 @@
    17.4    val mk_collect_set_map_tac: thm list -> tactic
    17.5    val mk_map_id': thm -> thm
    17.6    val mk_map_comp': thm -> thm
    17.7 -  val mk_map_cong_tac: thm -> tactic
    17.8 +  val mk_map_cong_tac: Proof.context -> thm -> tactic
    17.9    val mk_in_mono_tac: int -> tactic
   17.10    val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   17.11    val mk_set_map': thm -> thm
   17.12 @@ -36,8 +36,8 @@
   17.13  
   17.14  fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
   17.15  fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
   17.16 -fun mk_map_cong_tac cong0 =
   17.17 -  (hyp_subst_tac THEN' rtac cong0 THEN'
   17.18 +fun mk_map_cong_tac ctxt cong0 =
   17.19 +  (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
   17.20     REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
   17.21  fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
   17.22  fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
   17.23 @@ -82,21 +82,21 @@
   17.24        EVERY' [rtac equalityI, rtac subsetI,
   17.25          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   17.26          REPEAT_DETERM o dtac Pair_eqD,
   17.27 -        REPEAT_DETERM o etac conjE, hyp_subst_tac,
   17.28 +        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   17.29          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
   17.30          rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
   17.31          REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
   17.32 -          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   17.33 +          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   17.34            rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
   17.35            rtac (@{thm snd_conv} RS sym)],
   17.36          rtac CollectI,
   17.37          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   17.38            rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
   17.39 -          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   17.40 +          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   17.41            stac @{thm fst_conv}, atac]) set_maps,
   17.42          rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
   17.43          REPEAT_DETERM o dtac Pair_eqD,
   17.44 -        REPEAT_DETERM o etac conjE, hyp_subst_tac,
   17.45 +        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   17.46          rtac @{thm relcompI}, rtac @{thm converseI},
   17.47          EVERY' (map2 (fn convol => fn map_id =>
   17.48            EVERY' [rtac CollectI, rtac exI, rtac conjI,
   17.49 @@ -136,7 +136,7 @@
   17.50        EVERY' [rtac @{thm subrelI},
   17.51          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   17.52          REPEAT_DETERM o dtac Pair_eqD,
   17.53 -        REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
   17.54 +        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
   17.55          rtac @{thm relcompI}, rtac @{thm converseI},
   17.56          EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
   17.57            rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
   17.58 @@ -163,7 +163,7 @@
   17.59        EVERY' [rtac equalityI, rtac @{thm subrelI},
   17.60          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   17.61          REPEAT_DETERM o dtac Pair_eqD,
   17.62 -        REPEAT_DETERM o etac conjE, hyp_subst_tac,
   17.63 +        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   17.64          rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
   17.65          rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
   17.66          rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
   17.67 @@ -188,7 +188,7 @@
   17.68          REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
   17.69          REPEAT_DETERM o eresolve_tac [exE, conjE],
   17.70          REPEAT_DETERM o dtac Pair_eqD,
   17.71 -        REPEAT_DETERM o etac conjE, hyp_subst_tac,
   17.72 +        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   17.73          rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
   17.74          CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
   17.75          etac allE, etac impE, etac conjI, etac conjI, atac,
   17.76 @@ -206,7 +206,7 @@
   17.77    in
   17.78      unfold_thms_tac ctxt (srel_O_Grs @
   17.79        @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
   17.80 -    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
   17.81 +    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
   17.82        rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
   17.83        REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
   17.84        REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
    18.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    18.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    18.3 @@ -128,19 +128,19 @@
    18.4        (if is_refl disc then all_tac else rtac disc 1))
    18.5      (map rtac case_splits' @ [K all_tac]) corec_likes discs);
    18.6  
    18.7 -val solve_prem_prem_tac =
    18.8 +fun solve_prem_prem_tac ctxt =
    18.9    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
   18.10 -    hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   18.11 +    hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   18.12    (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
   18.13  
   18.14  fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs =
   18.15    EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
   18.16       SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)),
   18.17 -     solve_prem_prem_tac]) (rev kks)) 1;
   18.18 +     solve_prem_prem_tac ctxt]) (rev kks)) 1;
   18.19  
   18.20  fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks =
   18.21    let val r = length kks in
   18.22 -    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
   18.23 +    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
   18.24        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
   18.25      EVERY [REPEAT_DETERM_N r
   18.26          (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
   18.27 @@ -156,7 +156,7 @@
   18.28    end;
   18.29  
   18.30  fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
   18.31 -  hyp_subst_tac THEN'
   18.32 +  hyp_subst_tac ctxt THEN'
   18.33    CONVERSION (hhf_concl_conv
   18.34      (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
   18.35    SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
   18.36 @@ -164,17 +164,18 @@
   18.37    (atac ORELSE' REPEAT o etac conjE THEN'
   18.38       full_simp_tac
   18.39         (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN_MAYBE'
   18.40 -     REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
   18.41 +     REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
   18.42  
   18.43  fun mk_coinduct_distinct_ctrs ctxt discs discs' =
   18.44 -  hyp_subst_tac THEN' REPEAT o etac conjE THEN'
   18.45 +  hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
   18.46    full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
   18.47  
   18.48  fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
   18.49      discss selss =
   18.50    let val ks = 1 upto n in
   18.51      EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac
   18.52 -        meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1), hyp_subst_tac] @
   18.53 +        meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1),
   18.54 +        hyp_subst_tac ctxt] @
   18.55        map4 (fn k => fn ctr_def => fn discs => fn sels =>
   18.56          EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
   18.57            map2 (fn k' => fn discs' =>
    19.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Apr 27 11:37:50 2013 +0200
    19.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Apr 27 20:50:20 2013 +0200
    19.3 @@ -290,7 +290,7 @@
    19.4            prems concls xFs xFs_copy;
    19.5        in
    19.6          map (fn goal => Goal.prove_sorry lthy [] [] goal
    19.7 -          (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
    19.8 +          (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
    19.9        end;
   19.10  
   19.11      val timer = time (timer "Derived simple theorems");
   19.12 @@ -476,7 +476,7 @@
   19.13          Goal.prove_sorry lthy [] []
   19.14            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
   19.15              (Logic.list_implies (prems, concl)))
   19.16 -          (K ((hyp_subst_tac THEN' atac) 1))
   19.17 +          (K ((hyp_subst_tac lthy THEN' atac) 1))
   19.18          |> Thm.close_derivation
   19.19        end;
   19.20  
   19.21 @@ -847,7 +847,7 @@
   19.22          Goal.prove_sorry lthy [] []
   19.23            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
   19.24              (Logic.list_implies (prems, concl)))
   19.25 -          (K ((hyp_subst_tac THEN' atac) 1))
   19.26 +          (K ((hyp_subst_tac lthy THEN' atac) 1))
   19.27          |> Thm.close_derivation
   19.28        end;
   19.29  
   19.30 @@ -866,7 +866,7 @@
   19.31          Goal.prove_sorry lthy [] []
   19.32            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   19.33              (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
   19.34 -          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
   19.35 +          (K (mk_bis_srel_tac lthy m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
   19.36          |> Thm.close_derivation
   19.37        end;
   19.38  
   19.39 @@ -890,7 +890,7 @@
   19.40          Goal.prove_sorry lthy [] []
   19.41            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
   19.42              (Logic.list_implies (prems, concl)))
   19.43 -          (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os))
   19.44 +          (K (mk_bis_O_tac lthy m bis_srel_thm srel_congs srel_Os))
   19.45          |> Thm.close_derivation
   19.46        end;
   19.47  
   19.48 @@ -980,7 +980,7 @@
   19.49        Goal.prove_sorry lthy [] []
   19.50          (fold_rev Logic.all (As @ Bs @ ss)
   19.51            (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
   19.52 -        (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm))
   19.53 +        (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
   19.54        |> Thm.close_derivation;
   19.55  
   19.56      val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
   19.57 @@ -1299,7 +1299,7 @@
   19.58          val card_of_carT =
   19.59            Goal.prove_sorry lthy [] []
   19.60              (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
   19.61 -            (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm
   19.62 +            (K (mk_card_of_carT_tac lthy m isNode_defs sbd_sbd_thm
   19.63                sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
   19.64            |> Thm.close_derivation
   19.65        in
   19.66 @@ -1368,7 +1368,7 @@
   19.67                  map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss =>
   19.68                    singleton (Proof_Context.export names_lthy lthy)
   19.69                      (Goal.prove_sorry lthy [] [] goal
   19.70 -                      (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
   19.71 +                      (K (mk_strT_hset_tac lthy n m j arg_cong_cTs cTs cts
   19.72                          carT_defs strT_defs isNode_defs
   19.73                          set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
   19.74                          coalgT_thm set_map'ss)))
   19.75 @@ -1572,7 +1572,7 @@
   19.76  
   19.77          val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
   19.78            (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   19.79 -            (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
   19.80 +            (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss))
   19.81            |> Thm.close_derivation);
   19.82  
   19.83          val Lev_sbd' = mk_specN n Lev_sbd;
   19.84 @@ -1591,7 +1591,7 @@
   19.85  
   19.86          val length_Lev = singleton (Proof_Context.export names_lthy lthy)
   19.87            (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   19.88 -            (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
   19.89 +            (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
   19.90            |> Thm.close_derivation);
   19.91  
   19.92          val length_Lev' = mk_specN (n + 1) length_Lev;
   19.93 @@ -1621,7 +1621,7 @@
   19.94  
   19.95          val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
   19.96            (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   19.97 -            (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
   19.98 +            (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs)))
   19.99            |> Thm.close_derivation;
  19.100  
  19.101          val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
  19.102 @@ -1670,7 +1670,7 @@
  19.103          val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
  19.104            (Goal.prove_sorry lthy [] []
  19.105              (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
  19.106 -            (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  19.107 +            (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  19.108                coalg_set_thmss from_to_sbd_thmss)))
  19.109            |> Thm.close_derivation;
  19.110  
  19.111 @@ -1710,7 +1710,7 @@
  19.112  
  19.113          val set_Lev = singleton (Proof_Context.export names_lthy lthy)
  19.114            (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  19.115 -            (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
  19.116 +            (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
  19.117            |> Thm.close_derivation;
  19.118  
  19.119          val set_Lev' = mk_specN (3 * n + 1) set_Lev;
  19.120 @@ -1748,7 +1748,7 @@
  19.121  
  19.122          val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
  19.123            (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  19.124 -            (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  19.125 +            (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
  19.126                from_to_sbd_thmss to_sbd_inj_thmss)))
  19.127            |> Thm.close_derivation;
  19.128  
  19.129 @@ -2289,7 +2289,9 @@
  19.130          val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
  19.131            (Goal.prove_sorry lthy [] []
  19.132              (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
  19.133 -            (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
  19.134 +            (fn _ =>
  19.135 +              mk_dtor_srel_strong_coinduct_tac lthy
  19.136 +                m cTs cts dtor_srel_coinduct srel_monos srel_Ids))
  19.137            |> Thm.close_derivation;
  19.138  
  19.139          val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
  19.140 @@ -2584,7 +2586,7 @@
  19.141  
  19.142              val thm = singleton (Proof_Context.export names_lthy lthy)
  19.143                (Goal.prove_sorry lthy [] [] goal
  19.144 -              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
  19.145 +              (K (mk_mcong_tac lthy m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
  19.146                set_hset_thmss set_hset_hset_thmsss)))
  19.147                |> Thm.close_derivation
  19.148            in
  19.149 @@ -2696,7 +2698,8 @@
  19.150  
  19.151          val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
  19.152              fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
  19.153 -          K (mk_in_bd_tac (nth isNode_hsets (i - 1)) isNode_hsets carT_def
  19.154 +          K (mk_in_bd_tac lthy (* FIXME proper context!? *)
  19.155 +            (nth isNode_hsets (i - 1)) isNode_hsets carT_def
  19.156              card_of_carT mor_image Rep_inverse mor_hsets
  19.157              sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
  19.158            ks isNode_hset_thmss carT_defs card_of_carT_thms
  19.159 @@ -2944,7 +2947,7 @@
  19.160                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
  19.161                fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
  19.162                Goal.prove_sorry lthy [] [] goal
  19.163 -                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
  19.164 +                (K (mk_dtor_srel_tac lthy in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
  19.165                    dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
  19.166                |> Thm.close_derivation)
  19.167              ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
    20.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    20.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    20.3 @@ -9,18 +9,21 @@
    20.4  
    20.5  signature BNF_GFP_TACTICS =
    20.6  sig
    20.7 -  val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic
    20.8 +  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
    20.9 +    thm list list -> tactic
   20.10    val mk_bd_card_order_tac: thm -> tactic
   20.11    val mk_bd_cinfinite_tac: thm -> tactic
   20.12    val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
   20.13      {prems: 'a, context: Proof.context} -> tactic
   20.14 -  val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
   20.15 +  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   20.16    val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   20.17    val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
   20.18 -  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   20.19 +  val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
   20.20 +    thm list list -> tactic
   20.21    val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
   20.22      {prems: 'a, context: Proof.context} -> tactic
   20.23 -  val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
   20.24 +  val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
   20.25 +    thm list -> tactic
   20.26    val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
   20.27      {prems: 'a, context: Proof.context} -> tactic
   20.28    val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
   20.29 @@ -44,25 +47,25 @@
   20.30      thm -> thm -> tactic
   20.31    val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   20.32    val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   20.33 -  val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
   20.34 -    thm list -> thm list -> tactic
   20.35 -  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
   20.36 -    thm list -> thm list -> thm list list -> tactic
   20.37 +  val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
   20.38 +    cterm option list -> thm -> thm list -> thm list -> tactic
   20.39 +  val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
   20.40 +    thm -> thm -> thm list -> thm list -> thm list list -> tactic
   20.41    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
   20.42      {prems: 'a, context: Proof.context} -> tactic
   20.43    val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
   20.44    val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
   20.45    val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
   20.46      {prems: 'a, context: Proof.context} -> tactic
   20.47 -  val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
   20.48 -    thm -> thm -> thm -> tactic
   20.49 +  val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
   20.50 +    thm -> thm -> thm -> thm -> thm -> thm -> tactic
   20.51    val mk_incl_lsbis_tac: int -> int -> thm -> tactic
   20.52    val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   20.53    val mk_length_Lev'_tac: thm -> tactic
   20.54 -  val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
   20.55 +  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   20.56    val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
   20.57 -  val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
   20.58 -    thm list list -> thm list list list -> tactic
   20.59 +  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
   20.60 +    thm list list -> thm list list -> thm list list list -> tactic
   20.61    val mk_map_id_tac: thm list -> thm -> thm -> tactic
   20.62    val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
   20.63    val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   20.64 @@ -92,7 +95,7 @@
   20.65      {prems: 'a, context: Proof.context} -> tactic
   20.66    val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
   20.67      thm list -> tactic
   20.68 -  val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
   20.69 +  val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   20.70    val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
   20.71    val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
   20.72      thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
   20.73 @@ -100,22 +103,22 @@
   20.74    val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
   20.75      thm list -> thm list -> thm -> thm list -> tactic
   20.76    val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   20.77 -  val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
   20.78 -  val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
   20.79 -    thm list list -> tactic
   20.80 +  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
   20.81 +  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
   20.82 +    thm list -> thm list list -> tactic
   20.83    val mk_set_bd_tac: thm -> thm -> thm -> tactic
   20.84    val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
   20.85 -  val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
   20.86 -    thm list list -> thm list list -> tactic
   20.87 +  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
   20.88 +    thm list -> thm list -> thm list list -> thm list list -> tactic
   20.89    val mk_set_incl_hin_tac: thm list -> tactic
   20.90    val mk_set_incl_hset_tac: thm -> thm -> tactic
   20.91    val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   20.92    val mk_set_map_tac: thm -> thm -> tactic
   20.93 -  val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
   20.94 -    thm list list -> thm list list -> tactic
   20.95 -  val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
   20.96 -    cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
   20.97 -    thm list list -> thm list list -> thm -> thm list list -> tactic
   20.98 +  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
   20.99 +    thm list -> thm list -> thm list list -> thm list list -> tactic
  20.100 +  val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
  20.101 +    ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
  20.102 +    thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
  20.103    val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
  20.104    val mk_unique_mor_tac: thm list -> thm -> tactic
  20.105    val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
  20.106 @@ -256,7 +259,7 @@
  20.107    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
  20.108      atac, atac, rtac (hset_def RS sym)] 1
  20.109  
  20.110 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
  20.111 +fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
  20.112    let
  20.113      val n = length srel_O_Grs;
  20.114      val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
  20.115 @@ -288,7 +291,7 @@
  20.116          REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
  20.117          REPEAT_DETERM o dtac Pair_eqD,
  20.118          REPEAT_DETERM o etac conjE,
  20.119 -        hyp_subst_tac,
  20.120 +        hyp_subst_tac ctxt,
  20.121          REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  20.122          rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
  20.123          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
  20.124 @@ -327,7 +330,7 @@
  20.125          REPEAT_DETERM o etac allE,
  20.126          rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
  20.127  
  20.128 -fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
  20.129 +fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
  20.130    EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
  20.131      REPEAT_DETERM o etac conjE, rtac conjI,
  20.132      CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
  20.133 @@ -339,7 +342,7 @@
  20.134          rtac srel_O,
  20.135          etac @{thm relcompE},
  20.136          REPEAT_DETERM o dtac Pair_eqD,
  20.137 -        etac conjE, hyp_subst_tac,
  20.138 +        etac conjE, hyp_subst_tac ctxt,
  20.139          REPEAT_DETERM o etac allE, rtac @{thm relcompI},
  20.140          etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
  20.141  
  20.142 @@ -371,13 +374,13 @@
  20.143            atac]) (ks ~~ in_monos)] 1
  20.144    end;
  20.145  
  20.146 -fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
  20.147 +fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
  20.148    let
  20.149      val n = length lsbis_defs;
  20.150    in
  20.151      EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
  20.152        rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
  20.153 -      hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
  20.154 +      hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
  20.155    end;
  20.156  
  20.157  fun mk_incl_lsbis_tac n i lsbis_def =
  20.158 @@ -407,7 +410,7 @@
  20.159      val ks = 1 upto n;
  20.160      fun coalg_tac (i, ((passive_sets, active_sets), def)) =
  20.161        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
  20.162 -        hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
  20.163 +        hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
  20.164          rtac (mk_sum_casesN n i), rtac CollectI,
  20.165          EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
  20.166            etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
  20.167 @@ -449,7 +452,7 @@
  20.168      CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
  20.169    end;
  20.170  
  20.171 -fun mk_card_of_carT_tac m isNode_defs sbd_sbd
  20.172 +fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
  20.173    sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
  20.174    let
  20.175      val n = length isNode_defs;
  20.176 @@ -518,11 +521,11 @@
  20.177        if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
  20.178        rtac sbd_Cnotzero,
  20.179        rtac @{thm card_of_mono1}, rtac subsetI,
  20.180 -      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
  20.181 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
  20.182        rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
  20.183        rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
  20.184        rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
  20.185 -      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
  20.186 +      hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
  20.187        rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
  20.188        CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
  20.189          [rtac (mk_UnIN n i), dtac (def RS iffD1),
  20.190 @@ -538,7 +541,7 @@
  20.191    EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
  20.192      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
  20.193      dtac Pair_eqD,
  20.194 -    etac conjE, hyp_subst_tac,
  20.195 +    etac conjE, hyp_subst_tac ctxt,
  20.196      dtac (isNode_def RS iffD1),
  20.197      REPEAT_DETERM o eresolve_tac [exE, conjE],
  20.198      rtac (equalityD2 RS set_mp),
  20.199 @@ -548,7 +551,7 @@
  20.200      rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
  20.201      etac @{thm prefCl_Succ}, atac] 1;
  20.202  
  20.203 -fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
  20.204 +fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
  20.205    set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
  20.206    let
  20.207      val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
  20.208 @@ -564,7 +567,7 @@
  20.209          else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
  20.210            REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
  20.211            dtac conjunct2, dtac Pair_eqD, etac conjE,
  20.212 -          hyp_subst_tac, dtac (isNode_def RS iffD1),
  20.213 +          hyp_subst_tac ctxt, dtac (isNode_def RS iffD1),
  20.214            REPEAT_DETERM o eresolve_tac [exE, conjE],
  20.215            rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
  20.216        (ks ~~ (carT_defs ~~ isNode_defs));
  20.217 @@ -601,7 +604,7 @@
  20.218          (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
  20.219    end;
  20.220  
  20.221 -fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
  20.222 +fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
  20.223    let
  20.224      val n = length Lev_0s;
  20.225      val ks = 1 upto n;
  20.226 @@ -615,7 +618,7 @@
  20.227          EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
  20.228            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  20.229              (fn (i, to_sbd) => EVERY' [rtac subsetI,
  20.230 -              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.231 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.232                rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
  20.233                etac set_rev_mp, REPEAT_DETERM o etac allE,
  20.234                etac (mk_conjunctN n i)])
  20.235 @@ -623,7 +626,7 @@
  20.236        (Lev_Sucs ~~ to_sbdss)] 1
  20.237    end;
  20.238  
  20.239 -fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
  20.240 +fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
  20.241    let
  20.242      val n = length Lev_0s;
  20.243      val ks = n downto 1;
  20.244 @@ -637,16 +640,17 @@
  20.245        CONJ_WRAP' (fn Lev_Suc =>
  20.246          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
  20.247            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.248 -            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.249 -              rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
  20.250 -              REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
  20.251 +            (fn i =>
  20.252 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.253 +                rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
  20.254 +                REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
  20.255        Lev_Sucs] 1
  20.256    end;
  20.257  
  20.258  fun mk_length_Lev'_tac length_Lev =
  20.259    EVERY' [ftac length_Lev, etac ssubst, atac] 1;
  20.260  
  20.261 -fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
  20.262 +fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
  20.263    let
  20.264      val n = length Lev_0s;
  20.265      val ks = n downto 1;
  20.266 @@ -655,18 +659,21 @@
  20.267        REPEAT_DETERM o rtac allI,
  20.268        CONJ_WRAP' (fn Lev_0 =>
  20.269          EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
  20.270 -          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
  20.271 -          hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
  20.272 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
  20.273 +          dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
  20.274 +          hyp_subst_tac ctxt,
  20.275 +          rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
  20.276            rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
  20.277        REPEAT_DETERM o rtac allI,
  20.278        CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
  20.279          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
  20.280            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.281 -            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.282 -              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
  20.283 +            (fn i =>
  20.284 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.285 +              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
  20.286                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
  20.287                rtac Lev_0, rtac @{thm singletonI},
  20.288 -              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
  20.289 +              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
  20.290                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
  20.291                rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
  20.292                rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
  20.293 @@ -699,7 +706,7 @@
  20.294        ks)] 1
  20.295    end;
  20.296  
  20.297 -fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
  20.298 +fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
  20.299    let
  20.300      val n = length Lev_0s;
  20.301      val ks = 1 upto n;
  20.302 @@ -718,7 +725,7 @@
  20.303          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
  20.304            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.305              (fn (i, (from_to_sbd, coalg_set)) =>
  20.306 -              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.307 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.308                rtac (rv_Cons RS arg_cong RS iffD2),
  20.309                rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
  20.310                etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
  20.311 @@ -728,7 +735,7 @@
  20.312        ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
  20.313    end;
  20.314  
  20.315 -fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
  20.316 +fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
  20.317    let
  20.318      val n = length Lev_0s;
  20.319      val ks = 1 upto n;
  20.320 @@ -737,10 +744,10 @@
  20.321        REPEAT_DETERM o rtac allI,
  20.322        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
  20.323          EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
  20.324 -          etac @{thm singletonE}, hyp_subst_tac,
  20.325 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
  20.326            CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
  20.327              (if i = i'
  20.328 -            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
  20.329 +            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
  20.330                CONJ_WRAP' (fn (i'', Lev_0'') =>
  20.331                  EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
  20.332                    rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
  20.333 @@ -756,7 +763,7 @@
  20.334          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
  20.335            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.336              (fn (i, from_to_sbd) =>
  20.337 -              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.338 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.339                  CONJ_WRAP' (fn i' => rtac impI THEN'
  20.340                    CONJ_WRAP' (fn i'' =>
  20.341                      EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
  20.342 @@ -774,7 +781,7 @@
  20.343        ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
  20.344    end;
  20.345  
  20.346 -fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
  20.347 +fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
  20.348    let
  20.349      val n = length Lev_0s;
  20.350      val ks = 1 upto n;
  20.351 @@ -783,18 +790,18 @@
  20.352        REPEAT_DETERM o rtac allI,
  20.353        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
  20.354          EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
  20.355 -          etac @{thm singletonE}, hyp_subst_tac,
  20.356 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
  20.357            CONJ_WRAP' (fn i' => rtac impI THEN'
  20.358              CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
  20.359                (if i = i''
  20.360                then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
  20.361                  dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
  20.362 -                hyp_subst_tac,
  20.363 +                hyp_subst_tac ctxt,
  20.364                  CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.365                    (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
  20.366                      dtac list_inject_iffD1 THEN' etac conjE THEN'
  20.367                      (if k = i'
  20.368 -                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
  20.369 +                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
  20.370                      else etac (mk_InN_not_InM i' k RS notE)))
  20.371                  (rev ks)]
  20.372                else etac (mk_InN_not_InM i'' i RS notE)))
  20.373 @@ -806,7 +813,7 @@
  20.374          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
  20.375            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
  20.376              (fn (i, (from_to_sbd, to_sbd_inj)) =>
  20.377 -              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
  20.378 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
  20.379                CONJ_WRAP' (fn i' => rtac impI THEN'
  20.380                  dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
  20.381                  dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
  20.382 @@ -816,7 +823,7 @@
  20.383                    (if k = i
  20.384                    then EVERY' [dtac (mk_InN_inject n i),
  20.385                      dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
  20.386 -                    atac, atac, hyp_subst_tac] THEN'
  20.387 +                    atac, atac, hyp_subst_tac ctxt] THEN'
  20.388                      CONJ_WRAP' (fn i'' =>
  20.389                        EVERY' [rtac impI, dtac (sym RS trans),
  20.390                          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
  20.391 @@ -875,7 +882,7 @@
  20.392                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
  20.393                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
  20.394                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
  20.395 -                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
  20.396 +                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
  20.397                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
  20.398                    if n = 1 then rtac refl else atac])
  20.399                (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
  20.400 @@ -901,7 +908,7 @@
  20.401                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
  20.402                    REPEAT_DETERM_N 4 o etac thin_rl,
  20.403                    rtac set_image_Lev,
  20.404 -                  atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
  20.405 +                  atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
  20.406                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
  20.407                    if n = 1 then rtac refl else atac])
  20.408                (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
  20.409 @@ -958,7 +965,7 @@
  20.410                  dtac list_inject_iffD1, etac conjE,
  20.411                  if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
  20.412                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
  20.413 -                  atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
  20.414 +                  atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
  20.415                  else etac (mk_InN_not_InM i' i'' RS notE)])
  20.416              (rev ks),
  20.417              rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
  20.418 @@ -973,7 +980,7 @@
  20.419                  dtac list_inject_iffD1, etac conjE,
  20.420                  if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
  20.421                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
  20.422 -                  atac, atac, hyp_subst_tac, atac]
  20.423 +                  atac, atac, hyp_subst_tac ctxt, atac]
  20.424                  else etac (mk_InN_not_InM i' i'' RS notE)])
  20.425              (rev ks),
  20.426              rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
  20.427 @@ -1132,11 +1139,11 @@
  20.428      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
  20.429        rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
  20.430  
  20.431 -fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
  20.432 +fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
  20.433    EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
  20.434      EVERY' (map2 (fn srel_mono => fn srel_Id =>
  20.435        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
  20.436 -        etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
  20.437 +        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
  20.438          REPEAT_DETERM_N m o rtac @{thm subset_refl},
  20.439          REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
  20.440          rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
  20.441 @@ -1220,7 +1227,7 @@
  20.442          replicate n (@{thm o_id} RS fun_cong))))
  20.443      maps map_comps map_cong0s)] 1;
  20.444  
  20.445 -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
  20.446 +fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
  20.447    set_hset_hsetsss =
  20.448    let
  20.449      val n = length map_comp's;
  20.450 @@ -1230,8 +1237,8 @@
  20.451        coinduct_tac] @
  20.452        maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
  20.453          set_hset_hsetss) =>
  20.454 -        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
  20.455 -         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
  20.456 +        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
  20.457 +         rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
  20.458           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
  20.459           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
  20.460           rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
  20.461 @@ -1309,7 +1316,7 @@
  20.462      @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
  20.463      ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
  20.464  
  20.465 -fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
  20.466 +fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
  20.467    sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
  20.468    let
  20.469      val n = length isNode_hsets;
  20.470 @@ -1331,7 +1338,7 @@
  20.471        rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
  20.472        rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
  20.473        ftac (carT_def RS equalityD1 RS set_mp),
  20.474 -      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
  20.475 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
  20.476        rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
  20.477        rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
  20.478        rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
  20.479 @@ -1371,7 +1378,7 @@
  20.480    CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
  20.481      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  20.482        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  20.483 -      hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  20.484 +      hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  20.485        EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  20.486        pickWP_assms_tac,
  20.487        SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
  20.488 @@ -1395,7 +1402,7 @@
  20.489        CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
  20.490          EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  20.491            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  20.492 -          hyp_subst_tac,
  20.493 +          hyp_subst_tac ctxt,
  20.494            SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
  20.495            rtac (map_comp RS trans),
  20.496            SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
  20.497 @@ -1412,7 +1419,7 @@
  20.498    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
  20.499    CONJ_WRAP' (fn (unfold, map_comp) =>
  20.500      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
  20.501 -      hyp_subst_tac,
  20.502 +      hyp_subst_tac ctxt,
  20.503        SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
  20.504        rtac refl])
  20.505    (unfolds ~~ map_comps) 1;
  20.506 @@ -1431,7 +1438,7 @@
  20.507        CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
  20.508          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  20.509            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  20.510 -          hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  20.511 +          hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  20.512            EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
  20.513            pickWP_assms_tac,
  20.514            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  20.515 @@ -1443,7 +1450,7 @@
  20.516            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
  20.517              EVERY' [rtac @{thm UN_least},
  20.518                SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
  20.519 -              etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
  20.520 +              etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
  20.521                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
  20.522            (ks ~~ rev (drop m set_maps))])
  20.523        (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
  20.524 @@ -1484,18 +1491,18 @@
  20.525          (eresolve_tac wit ORELSE'
  20.526          (dresolve_tac wit THEN'
  20.527            (etac FalseE ORELSE'
  20.528 -          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
  20.529 +          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
  20.530              K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
  20.531  
  20.532  fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
  20.533 -  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
  20.534 +  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
  20.535    unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
  20.536 -  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
  20.537 +  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
  20.538    ALLGOALS (TRY o
  20.539      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
  20.540  
  20.541 -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
  20.542 -  set_maps dtor_set_incls dtor_set_set_inclss =
  20.543 +fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
  20.544 +    dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
  20.545    let
  20.546      val m = length dtor_set_incls;
  20.547      val n = length dtor_set_set_inclss;
  20.548 @@ -1536,7 +1543,7 @@
  20.549                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  20.550                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  20.551                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  20.552 -                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  20.553 +                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  20.554              (rev (active_set_maps ~~ in_Jsrels))])
  20.555          (dtor_sets ~~ passive_set_maps),
  20.556          rtac conjI,
    21.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sat Apr 27 11:37:50 2013 +0200
    21.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sat Apr 27 20:50:20 2013 +0200
    21.3 @@ -294,7 +294,7 @@
    21.4        in
    21.5          map2 (fn goal => fn alg_set =>
    21.6            Goal.prove_sorry lthy [] []
    21.7 -            goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
    21.8 +            goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
    21.9            |> Thm.close_derivation)
   21.10          goals alg_set_thms
   21.11        end;
   21.12 @@ -420,7 +420,7 @@
   21.13          Goal.prove_sorry lthy [] []
   21.14            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
   21.15               (Logic.list_implies (prems, concl)))
   21.16 -          (K ((hyp_subst_tac THEN' atac) 1))
   21.17 +          (K ((hyp_subst_tac lthy THEN' atac) 1))
   21.18          |> Thm.close_derivation
   21.19        end;
   21.20  
   21.21 @@ -654,7 +654,7 @@
   21.22  
   21.23          val monos =
   21.24            map2 (fn goal => fn min_algs =>
   21.25 -            Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
   21.26 +            Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
   21.27              |> Thm.close_derivation)
   21.28            (map mk_mono_goal min_algss) min_algs_thms;
   21.29  
   21.30 @@ -1315,7 +1315,7 @@
   21.31        in
   21.32          (Goal.prove_sorry lthy [] []
   21.33            (fold_rev Logic.all (phis @ Izs) goal)
   21.34 -          (K (mk_ctor_induct_tac m set_map'ss init_induct_thm morE_thms mor_Abs_thm
   21.35 +          (K (mk_ctor_induct_tac lthy m set_map'ss init_induct_thm morE_thms mor_Abs_thm
   21.36              Rep_inverses Abs_inverses Reps))
   21.37          |> Thm.close_derivation,
   21.38          rev (Term.add_tfrees goal []))
   21.39 @@ -1677,7 +1677,7 @@
   21.40  
   21.41              val thm = singleton (Proof_Context.export names_lthy lthy)
   21.42                (Goal.prove_sorry lthy [] [] goal
   21.43 -              (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
   21.44 +              (K (mk_lfp_map_wpull_tac lthy m (rtac induct) map_wpulls ctor_map_thms
   21.45                  (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
   21.46                |> Thm.close_derivation;
   21.47            in
   21.48 @@ -1728,13 +1728,14 @@
   21.49                ctors (0 upto n - 1) witss
   21.50            end;
   21.51  
   21.52 -        fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
   21.53 +        fun wit_tac ctxt _ = mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
   21.54  
   21.55          val (Ibnfs, lthy) =
   21.56            fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
   21.57                fn T => fn wits => fn lthy =>
   21.58 -            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b
   21.59 -              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
   21.60 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac lthy) (SOME deads)
   21.61 +              map_b rel_b set_bs
   21.62 +              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
   21.63                lthy
   21.64              |> register_bnf (Local_Theory.full_name lthy b))
   21.65            tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
   21.66 @@ -1780,7 +1781,7 @@
   21.67                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
   21.68                fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
   21.69                Goal.prove_sorry lthy [] [] goal
   21.70 -               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
   21.71 +               (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
   21.72                   ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
   21.73                |> Thm.close_derivation)
   21.74              ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
    22.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
    22.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
    22.3 @@ -10,7 +10,7 @@
    22.4  sig
    22.5    val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
    22.6      thm list -> tactic
    22.7 -  val mk_alg_not_empty_tac: thm -> thm list -> thm list -> tactic
    22.8 +  val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
    22.9    val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
   22.10    val mk_alg_set_tac: thm -> tactic
   22.11    val mk_bd_card_order_tac: thm list -> tactic
   22.12 @@ -18,13 +18,13 @@
   22.13    val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
   22.14    val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic
   22.15    val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
   22.16 -  val mk_ctor_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list ->
   22.17 -    thm list -> tactic
   22.18 +  val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
   22.19 +    thm list -> thm list -> thm list -> tactic
   22.20    val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
   22.21      {prems: 'a, context: Proof.context} -> tactic
   22.22    val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
   22.23 -  val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
   22.24 -    thm list -> thm list -> thm list list -> tactic
   22.25 +  val mk_ctor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
   22.26 +    thm -> thm -> thm list -> thm list -> thm list list -> tactic
   22.27    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   22.28    val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
   22.29    val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
   22.30 @@ -38,8 +38,8 @@
   22.31    val mk_iso_alt_tac: thm list -> thm -> tactic
   22.32    val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   22.33    val mk_least_min_alg_tac: thm -> thm -> tactic
   22.34 -  val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
   22.35 -    thm list list list -> thm list -> tactic
   22.36 +  val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
   22.37 +    thm list list -> thm list list list -> thm list -> tactic
   22.38    val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
   22.39    val mk_map_id_tac: thm list -> thm -> tactic
   22.40    val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
   22.41 @@ -49,7 +49,7 @@
   22.42    val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
   22.43      thm -> thm -> thm -> thm -> thm -> thm -> tactic
   22.44    val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
   22.45 -  val mk_min_algs_mono_tac: thm -> tactic
   22.46 +  val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   22.47    val mk_min_algs_tac: thm -> thm list -> tactic
   22.48    val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
   22.49    val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
   22.50 @@ -73,7 +73,7 @@
   22.51      thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
   22.52    val mk_set_map_tac: thm -> tactic
   22.53    val mk_set_tac: thm -> tactic
   22.54 -  val mk_wit_tac: int -> thm list -> thm list -> tactic
   22.55 +  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
   22.56    val mk_wpull_tac: thm -> tactic
   22.57  end;
   22.58  
   22.59 @@ -95,13 +95,13 @@
   22.60    EVERY' [etac bspec, rtac CollectI] 1 THEN
   22.61    REPEAT_DETERM (etac conjI 1) THEN atac 1;
   22.62  
   22.63 -fun mk_alg_not_empty_tac alg_set alg_sets wits =
   22.64 -  (EVERY' [rtac notI, hyp_subst_tac, ftac alg_set] THEN'
   22.65 +fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
   22.66 +  (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
   22.67    REPEAT_DETERM o FIRST'
   22.68      [rtac subset_UNIV,
   22.69      EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
   22.70      EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
   22.71 -    EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac,
   22.72 +    EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
   22.73        FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
   22.74    etac @{thm emptyE}) 1;
   22.75  
   22.76 @@ -280,10 +280,10 @@
   22.77      CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
   22.78    end;
   22.79  
   22.80 -fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
   22.81 +fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
   22.82    rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2},
   22.83    rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac,
   22.84 -  rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac, rtac refl] 1;
   22.85 +  rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
   22.86  
   22.87  fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   22.88    suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
   22.89 @@ -384,7 +384,7 @@
   22.90      REPEAT_DETERM o etac conjE, atac] 1;
   22.91  
   22.92  fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
   22.93 -  EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
   22.94 +  EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
   22.95    unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
   22.96  
   22.97  fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
   22.98 @@ -531,7 +531,7 @@
   22.99      (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
  22.100    etac fold_unique_mor 1;
  22.101  
  22.102 -fun mk_ctor_induct_tac m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
  22.103 +fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
  22.104    let
  22.105      val n = length set_map'ss;
  22.106      val ks = 1 upto n;
  22.107 @@ -539,7 +539,7 @@
  22.108      fun mk_IH_tac Rep_inv Abs_inv set_map' =
  22.109        DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
  22.110          dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE,
  22.111 -        hyp_subst_tac, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
  22.112 +        hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
  22.113  
  22.114      fun mk_closed_tac (k, (morE, set_map's)) =
  22.115        EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
  22.116 @@ -680,7 +680,7 @@
  22.117      (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
  22.118    end;
  22.119  
  22.120 -fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
  22.121 +fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
  22.122    let
  22.123      val n = length wpulls;
  22.124      val ks = 1 upto n;
  22.125 @@ -718,7 +718,7 @@
  22.126            CONJ_WRAP' (K (rtac subset_refl)) ks,
  22.127          rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
  22.128          rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
  22.129 -        hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
  22.130 +        hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
  22.131          CONJ_WRAP' mk_subset ctor_sets];
  22.132    in
  22.133      (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1
  22.134 @@ -763,7 +763,7 @@
  22.135    EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
  22.136      rtac wpull, REPEAT_DETERM o atac] 1;
  22.137  
  22.138 -fun mk_wit_tac n ctor_set wit =
  22.139 +fun mk_wit_tac ctxt n ctor_set wit =
  22.140    REPEAT_DETERM (atac 1 ORELSE
  22.141      EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
  22.142      REPEAT_DETERM o
  22.143 @@ -771,10 +771,10 @@
  22.144          (eresolve_tac wit ORELSE'
  22.145          (dresolve_tac wit THEN'
  22.146            (etac FalseE ORELSE'
  22.147 -          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
  22.148 +          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
  22.149              REPEAT_DETERM_N n o etac UnE]))))] 1);
  22.150  
  22.151 -fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
  22.152 +fun mk_ctor_srel_tac ctxt in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
  22.153    ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
  22.154    let
  22.155      val m = length ctor_set_incls;
  22.156 @@ -821,7 +821,7 @@
  22.157                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
  22.158                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  22.159                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  22.160 -                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  22.161 +                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  22.162              (rev (active_set_maps ~~ in_Isrels))])
  22.163          (ctor_sets ~~ passive_set_maps),
  22.164          rtac conjI,
    23.1 --- a/src/HOL/Bali/AxSem.thy	Sat Apr 27 11:37:50 2013 +0200
    23.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Apr 27 20:50:20 2013 +0200
    23.3 @@ -693,7 +693,7 @@
    23.4  apply       (tactic "ALLGOALS strip_tac")
    23.5  apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
    23.6           etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
    23.7 -apply       (tactic "TRYALL hyp_subst_tac")
    23.8 +apply       (tactic "TRYALL (hyp_subst_tac @{context})")
    23.9  apply       (simp, rule ax_derivs.empty)
   23.10  apply      (drule subset_insertD)
   23.11  apply      (blast intro: ax_derivs.insert)
    24.1 --- a/src/HOL/HOL.thy	Sat Apr 27 11:37:50 2013 +0200
    24.2 +++ b/src/HOL/HOL.thy	Sat Apr 27 20:50:20 2013 +0200
    24.3 @@ -849,15 +849,15 @@
    24.4  let
    24.5    fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    24.6      | non_bool_eq _ = false;
    24.7 -  val hyp_subst_tac' =
    24.8 +  fun hyp_subst_tac' ctxt =
    24.9      SUBGOAL (fn (goal, i) =>
   24.10        if Term.exists_Const non_bool_eq goal
   24.11 -      then Hypsubst.hyp_subst_tac i
   24.12 +      then Hypsubst.hyp_subst_tac ctxt i
   24.13        else no_tac);
   24.14  in
   24.15    Hypsubst.hypsubst_setup
   24.16    (*prevent substitution on bool*)
   24.17 -  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
   24.18 +  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   24.19  end
   24.20  *}
   24.21  
    25.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 27 11:37:50 2013 +0200
    25.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 27 20:50:20 2013 +0200
    25.3 @@ -1082,7 +1082,7 @@
    25.4  
    25.5  fun Seq_case_tac ctxt s i =
    25.6    res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
    25.7 -  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
    25.8 +  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
    25.9  
   25.10  (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
   25.11  fun Seq_case_simp_tac ctxt s i =
   25.12 @@ -1103,7 +1103,7 @@
   25.13  
   25.14  fun pair_tac ctxt s =
   25.15    res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
   25.16 -  THEN' hyp_subst_tac THEN' asm_full_simp_tac ctxt;
   25.17 +  THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
   25.18  
   25.19  (* induction on a sequence of pairs with pairsplitting and simplification *)
   25.20  fun pair_induct_tac ctxt s rws i =
    26.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Apr 27 11:37:50 2013 +0200
    26.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Apr 27 20:50:20 2013 +0200
    26.3 @@ -201,7 +201,7 @@
    26.4  apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
    26.5  apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
    26.6    THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
    26.7 -apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
    26.8 +apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac @{context}])")
    26.9  
   26.10  -- "Level 7"
   26.11  -- "15 NewC"
   26.12 @@ -240,7 +240,7 @@
   26.13  
   26.14  -- "for FAss"
   26.15  apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
   26.16 -       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
   26.17 +       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
   26.18  
   26.19  -- "for if"
   26.20  apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
    27.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 27 11:37:50 2013 +0200
    27.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 27 20:50:20 2013 +0200
    27.3 @@ -1738,7 +1738,7 @@
    27.4                 rotate_tac ~1 1,
    27.5                 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
    27.6                    (put_simpset HOL_ss context addsimps flat distinct_thms)) 1] @
    27.7 -               (if null idxs then [] else [hyp_subst_tac 1,
    27.8 +               (if null idxs then [] else [hyp_subst_tac context 1,
    27.9                  SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
   27.10                    let
   27.11                      val SOME prem = find_first (can (HOLogic.dest_eq o
    28.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Apr 27 11:37:50 2013 +0200
    28.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Apr 27 20:50:20 2013 +0200
    28.3 @@ -536,11 +536,11 @@
    28.4  by (blast intro: analz_mono [THEN [2] rev_subsetD])
    28.5  
    28.6  method_setup valid_certificate_tac = {*
    28.7 -  Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
    28.8 +  Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
    28.9      (fn i =>
   28.10        EVERY [ftac @{thm Gets_certificate_valid} i,
   28.11               assume_tac i,
   28.12 -             etac conjE i, REPEAT (hyp_subst_tac i)])))
   28.13 +             etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
   28.14  *}
   28.15  
   28.16  text{*The @{text "(no_asm)"} attribute is essential, since it retains
    29.1 --- a/src/HOL/SET_Protocol/Purchase.thy	Sat Apr 27 11:37:50 2013 +0200
    29.2 +++ b/src/HOL/SET_Protocol/Purchase.thy	Sat Apr 27 20:50:20 2013 +0200
    29.3 @@ -481,9 +481,9 @@
    29.4  
    29.5  method_setup valid_certificate_tac = {*
    29.6    Args.goal_spec >> (fn quant =>
    29.7 -    K (SIMPLE_METHOD'' quant (fn i =>
    29.8 +    fn ctxt => SIMPLE_METHOD'' quant (fn i =>
    29.9        EVERY [ftac @{thm Gets_certificate_valid} i,
   29.10 -             assume_tac i, REPEAT (hyp_subst_tac i)])))
   29.11 +             assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))
   29.12  *}
   29.13  
   29.14  
    30.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Apr 27 11:37:50 2013 +0200
    30.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Apr 27 20:50:20 2013 +0200
    30.3 @@ -418,13 +418,13 @@
    30.4          val inj_thm =
    30.5            Goal.prove_sorry_global thy5 [] []
    30.6              (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
    30.7 -            (fn _ => EVERY
    30.8 +            (fn {context = ctxt, ...} => EVERY
    30.9                [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   30.10                 REPEAT (EVERY
   30.11                   [rtac allI 1, rtac impI 1,
   30.12                    Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
   30.13                    REPEAT (EVERY
   30.14 -                    [hyp_subst_tac 1,
   30.15 +                    [hyp_subst_tac ctxt 1,
   30.16                       rewrite_goals_tac rewrites,
   30.17                       REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   30.18                       (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   30.19 @@ -480,7 +480,7 @@
   30.20        if length descr = 1 then []
   30.21        else
   30.22          drop (length newTs) (Datatype_Aux.split_conj_thm
   30.23 -          (Goal.prove_sorry_global thy5 [] [] iso_t (fn _ => EVERY
   30.24 +          (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
   30.25               [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   30.26                REPEAT (rtac TrueI 1),
   30.27                rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
   30.28 @@ -489,7 +489,7 @@
   30.29                REPEAT (EVERY
   30.30                  [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   30.31                     maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
   30.32 -                 TRY (hyp_subst_tac 1),
   30.33 +                 TRY (hyp_subst_tac ctxt 1),
   30.34                   rtac (sym RS range_eqI) 1,
   30.35                   resolve_tac iso_char_thms 1])])));
   30.36  
   30.37 @@ -556,9 +556,9 @@
   30.38                 Lim_inject, Suml_inject, Sumr_inject])
   30.39        in
   30.40          Goal.prove_sorry_global thy5 [] [] t
   30.41 -          (fn _ => EVERY
   30.42 +          (fn {context = ctxt, ...} => EVERY
   30.43              [rtac iffI 1,
   30.44 -             REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   30.45 +             REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
   30.46               dresolve_tac rep_congs 1, dtac box_equals 1,
   30.47               REPEAT (resolve_tac rep_thms 1),
   30.48               REPEAT (eresolve_tac inj_thms 1),
    31.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Apr 27 11:37:50 2013 +0200
    31.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Apr 27 20:50:20 2013 +0200
    31.3 @@ -179,9 +179,9 @@
    31.4                  etac elim 1,
    31.5                  REPEAT_DETERM_N j distinct_tac,
    31.6                  TRY (dresolve_tac inject 1),
    31.7 -                REPEAT (etac conjE 1), hyp_subst_tac 1,
    31.8 +                REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
    31.9                  REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   31.10 -                TRY (hyp_subst_tac 1),
   31.11 +                TRY (hyp_subst_tac ctxt 1),
   31.12                  rtac refl 1,
   31.13                  REPEAT_DETERM_N (n - j - 1) distinct_tac],
   31.14                intrs, j + 1)
   31.15 @@ -403,14 +403,15 @@
   31.16      fun prove_nchotomy (t, exhaustion) =
   31.17        let
   31.18          (* For goal i, select the correct disjunct to attack, then prove it *)
   31.19 -        fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   31.20 -          | tac i n = rtac disjI2 i THEN tac i (n - 1);
   31.21 +        fun tac ctxt i 0 =
   31.22 +              EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
   31.23 +          | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
   31.24        in
   31.25          Goal.prove_sorry_global thy [] [] t
   31.26 -          (fn _ =>
   31.27 +          (fn {context = ctxt, ...} =>
   31.28              EVERY [rtac allI 1,
   31.29               Datatype_Aux.exh_tac (K exhaustion) 1,
   31.30 -             ALLGOALS (fn i => tac i (i - 1))])
   31.31 +             ALLGOALS (fn i => tac ctxt i (i - 1))])
   31.32        end;
   31.33  
   31.34      val nchotomys =
    32.1 --- a/src/HOL/Tools/inductive.ML	Sat Apr 27 11:37:50 2013 +0200
    32.2 +++ b/src/HOL/Tools/inductive.ML	Sat Apr 27 20:50:20 2013 +0200
    32.3 @@ -534,7 +534,7 @@
    32.4  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    32.5  
    32.6  fun simp_case_tac ctxt i =
    32.7 -  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac] i;
    32.8 +  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
    32.9  
   32.10  in
   32.11  
   32.12 @@ -724,7 +724,7 @@
   32.13           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
   32.14           (*Now break down the individual cases.  No disjE here in case
   32.15             some premise involves disjunction.*)
   32.16 -         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
   32.17 +         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
   32.18           REPEAT (FIRSTGOAL
   32.19             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
   32.20           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
    33.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Apr 27 11:37:50 2013 +0200
    33.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Apr 27 20:50:20 2013 +0200
    33.3 @@ -317,7 +317,7 @@
    33.4  fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
    33.5    THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
    33.6    THEN' REPEAT_DETERM o etac @{thm conjE}
    33.7 -  THEN' TRY o hyp_subst_tac' ctxt;
    33.8 +  THEN' TRY o hyp_subst_tac ctxt;
    33.9  
   33.10  fun intro_image_tac ctxt = rtac @{thm image_eqI}
   33.11      THEN' (REPEAT_DETERM1 o
   33.12 @@ -332,7 +332,7 @@
   33.13    THEN' REPEAT_DETERM o CHANGED o
   33.14      (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
   33.15      THEN' REPEAT_DETERM o etac @{thm Pair_inject}
   33.16 -    THEN' TRY o hyp_subst_tac' ctxt)
   33.17 +    THEN' TRY o hyp_subst_tac ctxt)
   33.18  
   33.19  fun tac1_of_formula ctxt (Int (fm1, fm2)) =
   33.20      TRY o etac @{thm conjE}
   33.21 @@ -376,16 +376,16 @@
   33.22         ORELSE' etac @{thm conjE}
   33.23         ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
   33.24           TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
   33.25 -         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})
   33.26 +         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
   33.27         ORELSE' (etac @{thm imageE}
   33.28           THEN' (REPEAT_DETERM o CHANGED o
   33.29           (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
   33.30           THEN' REPEAT_DETERM o etac @{thm Pair_inject}
   33.31 -         THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})))
   33.32 +         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
   33.33         ORELSE' etac @{thm ComplE}
   33.34         ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
   33.35          THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
   33.36 -        THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl}))
   33.37 +        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
   33.38  
   33.39  fun tac ctxt fm =
   33.40    let
   33.41 @@ -398,7 +398,7 @@
   33.42        THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
   33.43        THEN' REPEAT_DETERM o resolve_tac @{thms exI}
   33.44        THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
   33.45 -      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac' ctxt) THEN' rtac @{thm refl}))))
   33.46 +      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
   33.47        THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
   33.48          REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
   33.49    in
    34.1 --- a/src/Provers/classical.ML	Sat Apr 27 11:37:50 2013 +0200
    34.2 +++ b/src/Provers/classical.ML	Sat Apr 27 20:50:20 2013 +0200
    34.3 @@ -25,8 +25,8 @@
    34.4    val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
    34.5    val classical: thm  (* (~ P ==> P) ==> P *)
    34.6    val sizef: thm -> int  (* size function for BEST_FIRST, typically size_of_thm *)
    34.7 -  val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
    34.8 -    the hypotheses; assumed to be safe! *)
    34.9 +  val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for
   34.10 +    substitution in the hypotheses; assumed to be safe! *)
   34.11  end;
   34.12  
   34.13  signature BASIC_CLASSICAL =
   34.14 @@ -697,7 +697,7 @@
   34.15         [eq_assume_tac,
   34.16          eq_mp_tac,
   34.17          bimatch_from_nets_tac safe0_netpair,
   34.18 -        FIRST' Data.hyp_subst_tacs,
   34.19 +        FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
   34.20          bimatch_from_nets_tac safep_netpair])
   34.21    end;
   34.22  
   34.23 @@ -733,7 +733,7 @@
   34.24       (FIRST'
   34.25         [eq_assume_contr_tac,
   34.26          bimatch_from_nets_tac safe0_netpair,
   34.27 -        FIRST' Data.hyp_subst_tacs,
   34.28 +        FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
   34.29          n_bimatch_from_nets_tac 1 safep_netpair,
   34.30          bimatch2_tac safep_netpair])
   34.31    end;
    35.1 --- a/src/Provers/hypsubst.ML	Sat Apr 27 11:37:50 2013 +0200
    35.2 +++ b/src/Provers/hypsubst.ML	Sat Apr 27 20:50:20 2013 +0200
    35.3 @@ -46,9 +46,8 @@
    35.4  
    35.5  signature HYPSUBST =
    35.6  sig
    35.7 -  val bound_hyp_subst_tac    : int -> tactic
    35.8 -  val hyp_subst_tac          : int -> tactic
    35.9 -  val hyp_subst_tac'         : Proof.context -> int -> tactic
   35.10 +  val bound_hyp_subst_tac    : Proof.context -> int -> tactic
   35.11 +  val hyp_subst_tac          : Proof.context -> int -> tactic
   35.12    val blast_hyp_subst_tac    : bool -> int -> tactic
   35.13    val stac                   : thm -> int -> tactic
   35.14    val hypsubst_setup         : theory -> theory
   35.15 @@ -127,14 +126,10 @@
   35.16  
   35.17    (*Select a suitable equality assumption; substitute throughout the subgoal
   35.18      If bnd is true, then it replaces Bound variables only. *)
   35.19 -  fun gen_hyp_subst_tac opt_ctxt bnd =
   35.20 +  fun gen_hyp_subst_tac ctxt bnd =
   35.21      let fun tac i st = SUBGOAL (fn (Bi, _) =>
   35.22        let
   35.23          val (k, _) = eq_var bnd true Bi
   35.24 -        val ctxt =
   35.25 -          (case opt_ctxt of
   35.26 -            NONE => Proof_Context.init_global (Thm.theory_of_thm st)
   35.27 -          | SOME ctxt => ctxt)
   35.28          val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
   35.29        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   35.30          etac thin_rl i, rotate_tac (~k) i]
   35.31 @@ -198,15 +193,13 @@
   35.32        handle THM _ => no_tac | EQ_VAR => no_tac);
   35.33  
   35.34  (*Substitutes for Free or Bound variables*)
   35.35 -val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   35.36 -        gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
   35.37 -
   35.38 -fun hyp_subst_tac' ctxt = FIRST' [ematch_tac [Data.thin_refl],
   35.39 -        gen_hyp_subst_tac (SOME ctxt) false, vars_gen_hyp_subst_tac false];
   35.40 +fun hyp_subst_tac ctxt =
   35.41 +  FIRST' [ematch_tac [Data.thin_refl],
   35.42 +    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
   35.43  
   35.44  (*Substitutes for Bound variables only -- this is always safe*)
   35.45 -val bound_hyp_subst_tac =
   35.46 -    gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
   35.47 +fun bound_hyp_subst_tac ctxt =
   35.48 +  gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
   35.49  
   35.50  
   35.51  (** Version for Blast_tac.  Hyps that are affected by the substitution are
   35.52 @@ -271,7 +264,7 @@
   35.53  
   35.54  val hypsubst_setup =
   35.55    Method.setup @{binding hypsubst}
   35.56 -    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
   35.57 +    (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   35.58      "substitution using an assumption (improper)" #>
   35.59    Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   35.60      "simple substitution";
    36.1 --- a/src/Pure/Isar/context_rules.ML	Sat Apr 27 11:37:50 2013 +0200
    36.2 +++ b/src/Pure/Isar/context_rules.ML	Sat Apr 27 20:50:20 2013 +0200
    36.3 @@ -14,8 +14,8 @@
    36.4    val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
    36.5    val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
    36.6    val print_rules: Proof.context -> unit
    36.7 -  val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    36.8 -  val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    36.9 +  val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
   36.10 +  val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
   36.11    val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
   36.12    val wrap: Proof.context -> (int -> tactic) -> int -> tactic
   36.13    val intro_bang: int option -> attribute
   36.14 @@ -68,8 +68,9 @@
   36.15   {next: int,
   36.16    rules: (int * ((int * bool) * thm)) list,
   36.17    netpairs: netpair list,
   36.18 -  wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
   36.19 -    (((int -> tactic) -> int -> tactic) * stamp) list};
   36.20 +  wrappers:
   36.21 +    ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
   36.22 +    ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list};
   36.23  
   36.24  fun make_rules next rules netpairs wrappers =
   36.25    Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
   36.26 @@ -170,7 +171,7 @@
   36.27  
   36.28  fun gen_wrap which ctxt =
   36.29    let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
   36.30 -  in fold_rev fst (which wrappers) end;
   36.31 +  in fold_rev (fn (w, _) => w ctxt) (which wrappers) end;
   36.32  
   36.33  val Swrap = gen_wrap #1;
   36.34  val wrap = gen_wrap #2;
    37.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Apr 27 11:37:50 2013 +0200
    37.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 27 20:50:20 2013 +0200
    37.3 @@ -231,7 +231,7 @@
    37.4       REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
    37.5                          ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
    37.6                                                type_elims)
    37.7 -                        ORELSE' hyp_subst_tac)),
    37.8 +                        ORELSE' hyp_subst_tac ctxt1)),
    37.9       if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
   37.10       else all_tac,
   37.11       DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   37.12 @@ -254,7 +254,7 @@
   37.13    (*Breaks down logical connectives in the monotonic function*)
   37.14    val basic_elim_tac =
   37.15        REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   37.16 -                ORELSE' bound_hyp_subst_tac))
   37.17 +                ORELSE' bound_hyp_subst_tac ctxt1))
   37.18        THEN prune_params_tac
   37.19            (*Mutual recursion: collapse references to Part(D,h)*)
   37.20        THEN (PRIMITIVE (fold_rule part_rec_defs));
   37.21 @@ -348,7 +348,7 @@
   37.22              (*Now break down the individual cases.  No disjE here in case
   37.23                some premise involves disjunction.*)
   37.24              REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
   37.25 -                               ORELSE' bound_hyp_subst_tac)),
   37.26 +                               ORELSE' (bound_hyp_subst_tac ctxt1))),
   37.27              ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   37.28  
   37.29       val dummy =