# HG changeset patch
# User wenzelm
# Date 1367088620 -7200
# Node ID ad3a241def734cb002ce62b7cd0830f55b03884c
# Parent  182454c06a80949cb69d7a6ed8a998a1d5393b06
uniform Proof.context for hyp_subst_tac;

diff -r 182454c06a80 -r ad3a241def73 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/CCL/Wfd.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -473,14 +473,11 @@
 
 (*** Clean up Correctness Condictions ***)
 
-val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
-                                 hyp_subst_tac)
-
 fun clean_ccs_tac ctxt =
   let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
     TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
-    eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
-    hyp_subst_tac))
+      eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
+      hyp_subst_tac ctxt))
   end
 
 fun gen_ccs_tac ctxt rls i =
diff -r 182454c06a80 -r ad3a241def73 src/Doc/ZF/IFOL_examples.thy
--- a/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Doc/ZF/IFOL_examples.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -36,7 +36,7 @@
 done
 
 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-by (tactic {*IntPr.fast_tac 1*})
+by (tactic {*IntPr.fast_tac @{context} 1*})
 
 text{*Example of Dyckhoff's method*}
 lemma "~ ~ ((P-->Q) | (Q-->P))"
diff -r 182454c06a80 -r ad3a241def73 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/FOL.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -150,7 +150,7 @@
   proof (rule r)
     { fix y y'
       assume "P(y)" and "P(y')"
-      with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+
+      with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
       then have "y = y'" by (rule subst)
     } note r' = this
     show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
diff -r 182454c06a80 -r ad3a241def73 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/IFOL.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -635,7 +635,7 @@
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
-setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
+setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *}
 
 
 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
diff -r 182454c06a80 -r ad3a241def73 src/FOL/ex/Intuitionistic.thy
--- a/src/FOL/ex/Intuitionistic.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Intuitionistic.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -17,7 +17,7 @@
 by (assume_tac 1);
 by (IntPr.safe_tac 1);
 by (IntPr.mp_tac 1);
-by (IntPr.fast_tac 1);
+by (IntPr.fast_tac @{context} 1);
 *)
 
 
@@ -37,55 +37,55 @@
 is intuitionstically equivalent to $P$.  [Andy Pitts] *}
 
 lemma "~~(P&Q) <-> ~~P & ~~Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*Double-negation does NOT distribute over disjunction*}
 
 lemma "~~(P-->Q)  <-> (~~P --> ~~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "~~~P <-> ~P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "(P<->Q) <-> (Q<->P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "((P --> (Q | (Q-->R))) --> R) --> R"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
       --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
       --> (((F-->A)-->B) --> I) --> E"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 text{*Lemmas for the propositional double-negation translation*}
 
 lemma "P --> ~~P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "~~(~~P --> P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "~~P & ~~(P --> Q) --> ~~Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 text{*The following are classically but not constructively valid.
       The attempt to prove them terminates quickly!*}
 lemma "((P-->Q) --> P)  -->  P"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
 lemma "(P&Q-->R)  -->  (P-->R) | (Q-->R)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
@@ -96,7 +96,7 @@
 lemma "((P<->Q) --> P&Q&R) &
                ((Q<->R) --> P&Q&R) &
                ((R<->P) --> P&Q&R) --> P&Q&R"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 text{*de Bruijn formula with five predicates*}
@@ -105,7 +105,7 @@
                ((R<->S) --> P&Q&R&S&T) &
                ((S<->T) --> P&Q&R&S&T) &
                ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 (*** Problems from of Sahlin, Franzen and Haridi,
@@ -116,11 +116,11 @@
 text{*Problem 1.1*}
 lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->
       (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
-by (tactic{*IntPr.best_dup_tac 1*})  --{*SLOW*}
+by (tactic{*IntPr.best_dup_tac @{context} 1*})  --{*SLOW*}
 
 text{*Problem 3.1*}
 lemma "~ (EX x. ALL y. mem(y,x) <-> ~ mem(x,x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*Problem 4.1: hopeless!*}
 lemma "(ALL x. p(x) --> p(h(x)) | p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))
@@ -132,78 +132,78 @@
 
 text{*~~1*}
 lemma "~~((P-->Q)  <->  (~Q --> ~P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~2*}
 lemma "~~(~~P  <->  P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*3*}
 lemma "~(P-->Q) --> (Q-->P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~4*}
 lemma "~~((~P-->Q)  <->  (~Q --> P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~5*}
 lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~6*}
 lemma "~~(P | ~P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~7*}
 lemma "~~(P | ~~~P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~8.  Peirce's law*}
 lemma "~~(((P-->Q) --> P)  -->  P)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*9*}
 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*10*}
 lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 subsection{*11.  Proved in each direction (incorrectly, says Pelletier!!) *}
 lemma "P<->P"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~12.  Dijkstra's law  *}
 lemma "~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*13.  Distributive law*}
 lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~14*}
 lemma "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~15*}
 lemma "~~((P --> Q) <-> (~P | Q))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~16*}
 lemma "~~((P-->Q) | (Q-->P))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~17*}
 lemma "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*Dijkstra's "Golden Rule"*}
 lemma "(P&Q) <-> P <-> Q <-> (P|Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 subsection{*****Examples with quantifiers*****}
@@ -212,19 +212,19 @@
 subsection{*The converse is classical in the following implications...*}
 
 lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 
 
@@ -233,28 +233,28 @@
 text{*The attempt to prove them terminates quickly!*}
 
 lemma "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
 lemma "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
 lemma "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
 lemma "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
 text{*Classically but not intuitionistically valid.  Proved by a bug in 1986!*}
 lemma "EX x. Q(x) --> (ALL x. Q(x))"
-apply (tactic{*IntPr.fast_tac 1*} | -)
+apply (tactic{*IntPr.fast_tac @{context} 1*} | -)
 apply (rule asm_rl) --{*Checks that subgoals remain: proof failed.*}
 oops
 
@@ -275,7 +275,7 @@
 text{*20*}
 lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
     --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*21*}
 lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"
@@ -283,11 +283,11 @@
 
 text{*22*}
 lemma "(ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~23*}
 lemma "~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*24*}
 lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
@@ -295,10 +295,10 @@
     --> ~~(EX x. P(x)&R(x))"
 txt{*Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and 
     @{text ITER_DEEPEN} all take forever*}
-apply (tactic{* IntPr.safe_tac*})
+apply (tactic{* IntPr.safe_tac @{context}*})
 apply (erule impE)
-apply (tactic{*IntPr.fast_tac 1*})
-by (tactic{*IntPr.fast_tac 1*})
+apply (tactic{*IntPr.fast_tac @{context} 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*25*}
 lemma "(EX x. P(x)) &
@@ -306,7 +306,7 @@
         (ALL x. P(x) --> (M(x) & L(x))) &
         ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
     --> (EX x. Q(x)&P(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~26*}
 lemma "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &
@@ -320,45 +320,45 @@
               (ALL x. M(x) & L(x) --> P(x)) &
               ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
           --> (ALL x. M(x) --> ~L(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~28.  AMENDED*}
 lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
         (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
         (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
     --> (ALL x. P(x) & L(x) --> M(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*29.  Essentially the same as Principia Mathematica *11.71*}
 lemma "(EX x. P(x)) & (EX y. Q(y))
     --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->
          (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~30*}
 lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
         (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
     --> (ALL x. ~~S(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*31*}
 lemma "~(EX x. P(x) & (Q(x) | R(x))) &
         (EX x. L(x) & P(x)) &
         (ALL x. ~ R(x) --> M(x))
     --> (EX x. L(x) & M(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*32*}
 lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
         (ALL x. S(x) & R(x) --> L(x)) &
         (ALL x. M(x) --> R(x))
     --> (ALL x. P(x) & M(x) --> L(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*~~33*}
 lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  <->
       (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
-apply (tactic{*IntPr.best_tac 1*})
+apply (tactic{*IntPr.best_tac @{context} 1*})
 done
 
 
@@ -367,7 +367,7 @@
       (ALL x. EX y. G(x,y)) &
       (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
   --> (ALL x. EX y. H(x,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*37*}
 lemma "(ALL z. EX w. ALL x. EX y.
@@ -379,47 +379,47 @@
 
 text{*39*}
 lemma "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*40.  AMENDED*}
 lemma "(EX y. ALL x. F(x,y) <-> F(x,x)) -->
               ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*44*}
 lemma "(ALL x. f(x) -->
               (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &
               (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
               --> (EX x. j(x) & ~f(x))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*48*}
 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*51*}
 lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
      (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*52*}
 text{*Almost the same as 51. *}
 lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
      (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*56*}
 lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*57*}
 lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
      (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 text{*60*}
 lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by (tactic{*IntPr.fast_tac 1*})
+by (tactic{*IntPr.fast_tac @{context} 1*})
 
 end
 
diff -r 182454c06a80 -r ad3a241def73 src/FOL/ex/Propositional_Cla.thy
--- a/src/FOL/ex/Propositional_Cla.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -12,7 +12,7 @@
 text {* commutative laws of @{text "&"} and @{text "|"} *}
 
 lemma "P & Q  -->  Q & P"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "P | Q  -->  Q | P"
   by fast
diff -r 182454c06a80 -r ad3a241def73 src/FOL/ex/Propositional_Int.thy
--- a/src/FOL/ex/Propositional_Int.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Propositional_Int.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -12,106 +12,106 @@
 text {* commutative laws of @{text "&"} and @{text "|"} *}
 
 lemma "P & Q  -->  Q & P"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "P | Q  -->  Q | P"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* associative laws of @{text "&"} and @{text "|"} *}
 lemma "(P & Q) & R  -->  P & (Q & R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P | Q) | R  -->  P | (Q | R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* distributive laws of @{text "&"} and @{text "|"} *}
 lemma "(P & Q) | R  --> (P | R) & (Q | R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P | R) & (Q | R)  --> (P & Q) | R"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P | Q) & R  --> (P & R) | (Q & R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P & R) | (Q & R)  --> (P | Q) & R"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Laws involving implication *}
 
 lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P & Q --> R) <-> (P--> (Q-->R))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P --> Q & R) <-> (P-->Q)  &  (P-->R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Propositions-as-types *}
 
 -- {* The combinator K *}
 lemma "P --> (Q --> P)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 -- {* The combinator S *}
 lemma "(P-->Q-->R)  --> (P-->Q) --> (P-->R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 -- {* Converse is classical *}
 lemma "(P-->Q) | (P-->R)  -->  (P --> Q | R)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(P-->Q)  -->  (~Q --> ~P)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Schwichtenberg's examples (via T. Nipkow) *}
 
 lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma stab_to_peirce:
   "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
                               --> ((P --> Q) --> P) --> P"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)  
                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
   
 lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)  
   --> (((P8 --> P2) --> P9) --> P3 --> P10)  
   --> (P1 --> P8) --> P6 --> P7  
   --> (((P3 --> P2) --> P9) --> P4)  
   --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)  
   --> (((P3 --> P2) --> P9) --> P4)  
   --> (((P6 --> P1) --> P2) --> P9)  
   --> (((P7 --> P1) --> P10) --> P4 --> P5)  
   --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 end
diff -r 182454c06a80 -r ad3a241def73 src/FOL/ex/Quantifiers_Int.thy
--- a/src/FOL/ex/Quantifiers_Int.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -10,91 +10,91 @@
 begin
 
 lemma "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 -- {* Converse is false *}
 lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 lemma "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Some harder ones *}
 
 lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 -- {* Converse is false *}
 lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Basic test of quantifier reasoning *}
 
 -- {* TRUE *}
 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* The following should fail, as they are false! *}
 
 lemma "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
-  apply (tactic "IntPr.fast_tac 1")?
+  apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
 lemma "(EX x. Q(x))  -->  (ALL x. Q(x))"
-  apply (tactic "IntPr.fast_tac 1")?
+  apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
 schematic_lemma "P(?a) --> (ALL x. P(x))"
-  apply (tactic "IntPr.fast_tac 1")?
+  apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
 schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
-  apply (tactic "IntPr.fast_tac 1")?
+  apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
 
 text {* Back to things that are provable \dots *}
 
 lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 -- {* An example of why exI should be delayed as long as possible *}
 lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text {* Some slow ones *}
 
 -- {* Principia Mathematica *11.53 *}
 lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 (*Principia Mathematica *11.55  *)
 lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 (*Principia Mathematica *11.61  *)
 lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 end
diff -r 182454c06a80 -r ad3a241def73 src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/intprover.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -16,19 +16,19 @@
 *)
 
 signature INT_PROVER = 
-  sig
-  val best_tac: int -> tactic
-  val best_dup_tac: int -> tactic
-  val fast_tac: int -> tactic
+sig
+  val best_tac: Proof.context -> int -> tactic
+  val best_dup_tac: Proof.context -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
   val inst_step_tac: int -> tactic
-  val safe_step_tac: int -> tactic
+  val safe_step_tac: Proof.context -> int -> tactic
   val safe_brls: (bool * thm) list
-  val safe_tac: tactic
-  val step_tac: int -> tactic
-  val step_dup_tac: int -> tactic
+  val safe_tac: Proof.context -> tactic
+  val step_tac: Proof.context -> int -> tactic
+  val step_dup_tac: Proof.context -> int -> tactic
   val haz_brls: (bool * thm) list
   val haz_dup_brls: (bool * thm) list
-  end;
+end;
 
 
 structure IntPr : INT_PROVER   = 
@@ -62,14 +62,16 @@
     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
-val safe_step_tac = FIRST' [eq_assume_tac,
-                            eq_mp_tac,
-                            bimatch_tac safe0_brls,
-                            hyp_subst_tac,
-                            bimatch_tac safep_brls] ;
+fun safe_step_tac ctxt =
+  FIRST' [
+    eq_assume_tac,
+    eq_mp_tac,
+    bimatch_tac safe0_brls,
+    hyp_subst_tac ctxt,
+    bimatch_tac safep_brls];
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
+fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 val inst_step_tac =
@@ -77,20 +79,20 @@
   biresolve_tac (safe0_brls @ safep_brls);
 
 (*One safe or unsafe step. *)
-fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
+fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i];
 
-fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
+fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i];
 
 (*Dumb but fast*)
-val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
+fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
-val best_tac = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
+fun best_tac ctxt =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
 
 (*Uses all_dupE: allows multiple use of universal assumptions.  VERY slow.*)
-val best_dup_tac = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1));
+fun best_dup_tac ctxt =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
 
 
 end;
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -258,9 +258,9 @@
 
 method_setup disentangle = {*
     Scan.succeed
-     (K (SIMPLE_METHOD
+     (fn ctxt => SIMPLE_METHOD
       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
-                   ORELSE' hyp_subst_tac)))) *}
+                   ORELSE' hyp_subst_tac ctxt))) *}
   "for eliminating conjunctions, disjunctions and the like"
 
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -751,11 +751,11 @@
  (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
  (*Base*)  (force_tac ctxt) 1
 
-val analz_prepare_tac = 
+fun analz_prepare_tac ctxt =
          prepare_tac THEN
          dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN 
  (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN 
-         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
+         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
 
 end
 *}
@@ -769,7 +769,7 @@
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.analz_prepare_tac ctxt)) *}
   "additional facts to reason about analz"
 
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -764,7 +764,7 @@
          prepare_tac ctxt THEN
          dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
  (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
-         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
+         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
 
 end
 *}
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -221,7 +221,7 @@
     REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
     (TRY o dresolve_tac Gwit_thms THEN'
     (etac FalseE ORELSE'
-    hyp_subst_tac THEN'
+    hyp_subst_tac ctxt THEN'
     dresolve_tac Fwit_thms THEN'
     (etac FalseE ORELSE' atac))) 1);
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -504,7 +504,7 @@
                   val half_goalss = map mk_goal half_pairss;
                   val half_thmss =
                     map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
-                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
+                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
                       half_goalss half_pairss (flat disc_thmss');
 
                   val other_half_goalss = map (mk_goal o map swap) half_pairss;
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -15,7 +15,7 @@
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
     thm list list list -> thm list list list -> tactic
-  val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
+  val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_disc_exclude_tac: thm -> tactic
   val mk_split_tac: Proof.context ->
@@ -44,13 +44,13 @@
 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
   EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
     rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
-    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+    hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
     rtac distinct, rtac uexhaust] @
     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
      |> k = 1 ? swap |> op @)) 1;
 
-fun mk_half_disc_exclude_tac m discD disc' =
-  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
+fun mk_half_disc_exclude_tac ctxt m discD disc' =
+  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' rtac disc') 1;
 
 fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
 
@@ -64,7 +64,7 @@
    (if m = 0 then
       atac
     else
-      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
+      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
 
 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
@@ -100,7 +100,7 @@
 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
   (rtac uexhaust THEN'
    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
-       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
+       EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
      cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
 
 fun mk_case_cong_tac ctxt uexhaust cases =
@@ -112,7 +112,7 @@
 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
 fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   rtac uexhaust 1 THEN
-  ALLGOALS (fn k => (hyp_subst_tac THEN'
+  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
      simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
        flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   ALLGOALS (blast_tac naked_ctxt);
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -971,7 +971,8 @@
                 (Logic.list_implies (prems_cong,
                   mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
           in
-            Goal.prove_sorry lthy [] [] in_cong_goal (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+            Goal.prove_sorry lthy [] [] in_cong_goal
+              (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1))
             |> Thm.close_derivation
           end;
 
@@ -989,7 +990,7 @@
             val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
               (Logic.list_implies (prem0 :: prems, eq));
           in
-            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac (#map_cong0 axioms))
+            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
             |> Thm.close_derivation
           end;
 
@@ -1073,7 +1074,7 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
-              (fn _ => (TRY o hyp_subst_tac THEN' rtac refl) 1)
+              (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1)
             |> Thm.close_derivation
           end;
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -11,7 +11,7 @@
   val mk_collect_set_map_tac: thm list -> tactic
   val mk_map_id': thm -> thm
   val mk_map_comp': thm -> thm
-  val mk_map_cong_tac: thm -> tactic
+  val mk_map_cong_tac: Proof.context -> thm -> tactic
   val mk_in_mono_tac: int -> tactic
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_map': thm -> thm
@@ -36,8 +36,8 @@
 
 fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
 fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
-fun mk_map_cong_tac cong0 =
-  (hyp_subst_tac THEN' rtac cong0 THEN'
+fun mk_map_cong_tac ctxt cong0 =
+  (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
    REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
 fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
 fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
@@ -82,21 +82,21 @@
       EVERY' [rtac equalityI, rtac subsetI,
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
-          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
           rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
           rtac (@{thm snd_conv} RS sym)],
         rtac CollectI,
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
           rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
-          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
           stac @{thm fst_conv}, atac]) set_maps,
         rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
         REPEAT_DETERM o dtac Pair_eqD,
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map2 (fn convol => fn map_id =>
           EVERY' [rtac CollectI, rtac exI, rtac conjI,
@@ -136,7 +136,7 @@
       EVERY' [rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
-        REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
           rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
@@ -163,7 +163,7 @@
       EVERY' [rtac equalityI, rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
         rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
         rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
@@ -188,7 +188,7 @@
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [exE, conjE],
         REPEAT_DETERM o dtac Pair_eqD,
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
         rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
         CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
         etac allE, etac impE, etac conjI, etac conjI, atac,
@@ -206,7 +206,7 @@
   in
     unfold_thms_tac ctxt (srel_O_Grs @
       @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
-    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
+    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
       rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
       REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
       REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -128,19 +128,19 @@
       (if is_refl disc then all_tac else rtac disc 1))
     (map rtac case_splits' @ [K all_tac]) corec_likes discs);
 
-val solve_prem_prem_tac =
+fun solve_prem_prem_tac ctxt =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
-    hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
+    hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
 
 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs =
   EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
      SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)),
-     solve_prem_prem_tac]) (rev kks)) 1;
+     solve_prem_prem_tac ctxt]) (rev kks)) 1;
 
 fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks =
   let val r = length kks in
-    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
+    EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
       REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
     EVERY [REPEAT_DETERM_N r
         (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
@@ -156,7 +156,7 @@
   end;
 
 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
-  hyp_subst_tac THEN'
+  hyp_subst_tac ctxt THEN'
   CONVERSION (hhf_concl_conv
     (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
@@ -164,17 +164,18 @@
   (atac ORELSE' REPEAT o etac conjE THEN'
      full_simp_tac
        (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN_MAYBE'
-     REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
+     REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
 
 fun mk_coinduct_distinct_ctrs ctxt discs discs' =
-  hyp_subst_tac THEN' REPEAT o etac conjE THEN'
+  hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
   full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
 
 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
     discss selss =
   let val ks = 1 upto n in
     EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac
-        meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1), hyp_subst_tac] @
+        meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1),
+        hyp_subst_tac ctxt] @
       map4 (fn k => fn ctr_def => fn discs => fn sels =>
         EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
           map2 (fn k' => fn discs' =>
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -290,7 +290,7 @@
           prems concls xFs xFs_copy;
       in
         map (fn goal => Goal.prove_sorry lthy [] [] goal
-          (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
+          (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
       end;
 
     val timer = time (timer "Derived simple theorems");
@@ -476,7 +476,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
             (Logic.list_implies (prems, concl)))
-          (K ((hyp_subst_tac THEN' atac) 1))
+          (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
       end;
 
@@ -847,7 +847,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
             (Logic.list_implies (prems, concl)))
-          (K ((hyp_subst_tac THEN' atac) 1))
+          (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
       end;
 
@@ -866,7 +866,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
             (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
-          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
+          (K (mk_bis_srel_tac lthy m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
         |> Thm.close_derivation
       end;
 
@@ -890,7 +890,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
             (Logic.list_implies (prems, concl)))
-          (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os))
+          (K (mk_bis_O_tac lthy m bis_srel_thm srel_congs srel_Os))
         |> Thm.close_derivation
       end;
 
@@ -980,7 +980,7 @@
       Goal.prove_sorry lthy [] []
         (fold_rev Logic.all (As @ Bs @ ss)
           (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
-        (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm))
+        (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
       |> Thm.close_derivation;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
@@ -1299,7 +1299,7 @@
         val card_of_carT =
           Goal.prove_sorry lthy [] []
             (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
-            (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm
+            (K (mk_card_of_carT_tac lthy m isNode_defs sbd_sbd_thm
               sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
           |> Thm.close_derivation
       in
@@ -1368,7 +1368,7 @@
                 map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss =>
                   singleton (Proof_Context.export names_lthy lthy)
                     (Goal.prove_sorry lthy [] [] goal
-                      (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
+                      (K (mk_strT_hset_tac lthy n m j arg_cong_cTs cTs cts
                         carT_defs strT_defs isNode_defs
                         set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
                         coalgT_thm set_map'ss)))
@@ -1572,7 +1572,7 @@
 
         val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
+            (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss))
           |> Thm.close_derivation);
 
         val Lev_sbd' = mk_specN n Lev_sbd;
@@ -1591,7 +1591,7 @@
 
         val length_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
+            (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
           |> Thm.close_derivation);
 
         val length_Lev' = mk_specN (n + 1) length_Lev;
@@ -1621,7 +1621,7 @@
 
         val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
+            (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs)))
           |> Thm.close_derivation;
 
         val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
@@ -1670,7 +1670,7 @@
         val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] []
             (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
-            (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
+            (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
               coalg_set_thmss from_to_sbd_thmss)))
           |> Thm.close_derivation;
 
@@ -1710,7 +1710,7 @@
 
         val set_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
+            (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
           |> Thm.close_derivation;
 
         val set_Lev' = mk_specN (3 * n + 1) set_Lev;
@@ -1748,7 +1748,7 @@
 
         val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss
+            (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
               from_to_sbd_thmss to_sbd_inj_thmss)))
           |> Thm.close_derivation;
 
@@ -2289,7 +2289,9 @@
         val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
-            (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
+            (fn _ =>
+              mk_dtor_srel_strong_coinduct_tac lthy
+                m cTs cts dtor_srel_coinduct srel_monos srel_Ids))
           |> Thm.close_derivation;
 
         val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2584,7 +2586,7 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
+              (K (mk_mcong_tac lthy m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
               set_hset_thmss set_hset_hset_thmsss)))
               |> Thm.close_derivation
           in
@@ -2696,7 +2698,8 @@
 
         val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
             fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
-          K (mk_in_bd_tac (nth isNode_hsets (i - 1)) isNode_hsets carT_def
+          K (mk_in_bd_tac lthy (* FIXME proper context!? *)
+            (nth isNode_hsets (i - 1)) isNode_hsets carT_def
             card_of_carT mor_image Rep_inverse mor_hsets
             sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
           ks isNode_hset_thmss carT_defs card_of_carT_thms
@@ -2944,7 +2947,7 @@
               fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
               fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
+                (K (mk_dtor_srel_tac lthy in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
                   dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -9,18 +9,21 @@
 
 signature BNF_GFP_TACTICS =
 sig
-  val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic
+  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
+    thm list list -> tactic
   val mk_bd_card_order_tac: thm -> tactic
   val mk_bd_cinfinite_tac: thm -> tactic
   val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
+  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
-  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
+  val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+    thm list list -> tactic
   val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
+  val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
+    thm list -> tactic
   val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
@@ -44,25 +47,25 @@
     thm -> thm -> tactic
   val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
-  val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
-    thm list -> thm list -> tactic
-  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
-    thm list -> thm list -> thm list list -> tactic
+  val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
+    cterm option list -> thm -> thm list -> thm list -> tactic
+  val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+    thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
   val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
-    thm -> thm -> thm -> tactic
+  val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
+    thm -> thm -> thm -> thm -> thm -> thm -> tactic
   val mk_incl_lsbis_tac: int -> int -> thm -> tactic
   val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_length_Lev'_tac: thm -> tactic
-  val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
+  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
-  val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
-    thm list list -> thm list list list -> tactic
+  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
+    thm list list -> thm list list -> thm list list list -> tactic
   val mk_map_id_tac: thm list -> thm -> thm -> tactic
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
   val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -92,7 +95,7 @@
     {prems: 'a, context: Proof.context} -> tactic
   val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
     thm list -> tactic
-  val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
+  val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
   val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
   val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
     thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
@@ -100,22 +103,22 @@
   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
     thm list -> thm list -> thm -> thm list -> tactic
   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
-  val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
-  val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
-    thm list list -> tactic
+  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
+  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
+    thm list -> thm list list -> tactic
   val mk_set_bd_tac: thm -> thm -> thm -> tactic
   val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
-  val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
-    thm list list -> thm list list -> tactic
+  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
+    thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_set_incl_hin_tac: thm list -> tactic
   val mk_set_incl_hset_tac: thm -> thm -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   val mk_set_map_tac: thm -> thm -> tactic
-  val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
-    thm list list -> thm list list -> tactic
-  val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
-    cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
-    thm list list -> thm list list -> thm -> thm list list -> tactic
+  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
+    thm list -> thm list -> thm list list -> thm list list -> tactic
+  val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
+    ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
+    thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_unique_mor_tac: thm list -> thm -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
@@ -256,7 +259,7 @@
   EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
     atac, atac, rtac (hset_def RS sym)] 1
 
-fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
+fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
   let
     val n = length srel_O_Grs;
     val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
@@ -288,7 +291,7 @@
         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE,
-        hyp_subst_tac,
+        hyp_subst_tac ctxt,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
         rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
@@ -327,7 +330,7 @@
         REPEAT_DETERM o etac allE,
         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
 
-fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
+fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
   EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
@@ -339,7 +342,7 @@
         rtac srel_O,
         etac @{thm relcompE},
         REPEAT_DETERM o dtac Pair_eqD,
-        etac conjE, hyp_subst_tac,
+        etac conjE, hyp_subst_tac ctxt,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
         etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
 
@@ -371,13 +374,13 @@
           atac]) (ks ~~ in_monos)] 1
   end;
 
-fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
+fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
   let
     val n = length lsbis_defs;
   in
     EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
       rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
-      hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
+      hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   end;
 
 fun mk_incl_lsbis_tac n i lsbis_def =
@@ -407,7 +410,7 @@
     val ks = 1 upto n;
     fun coalg_tac (i, ((passive_sets, active_sets), def)) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-        hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
+        hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_casesN n i), rtac CollectI,
         EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
           etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
@@ -449,7 +452,7 @@
     CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
   end;
 
-fun mk_card_of_carT_tac m isNode_defs sbd_sbd
+fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
   sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
   let
     val n = length isNode_defs;
@@ -518,11 +521,11 @@
       if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
       rtac sbd_Cnotzero,
       rtac @{thm card_of_mono1}, rtac subsetI,
-      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
+      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
       rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
       rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
       rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
-      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
+      hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
         [rtac (mk_UnIN n i), dtac (def RS iffD1),
@@ -538,7 +541,7 @@
   EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
     REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
     dtac Pair_eqD,
-    etac conjE, hyp_subst_tac,
+    etac conjE, hyp_subst_tac ctxt,
     dtac (isNode_def RS iffD1),
     REPEAT_DETERM o eresolve_tac [exE, conjE],
     rtac (equalityD2 RS set_mp),
@@ -548,7 +551,7 @@
     rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
     etac @{thm prefCl_Succ}, atac] 1;
 
-fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
+fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
   let
     val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
@@ -564,7 +567,7 @@
         else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
           dtac conjunct2, dtac Pair_eqD, etac conjE,
-          hyp_subst_tac, dtac (isNode_def RS iffD1),
+          hyp_subst_tac ctxt, dtac (isNode_def RS iffD1),
           REPEAT_DETERM o eresolve_tac [exE, conjE],
           rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
       (ks ~~ (carT_defs ~~ isNode_defs));
@@ -601,7 +604,7 @@
         (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
   end;
 
-fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
+fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
   let
     val n = length Lev_0s;
     val ks = 1 upto n;
@@ -615,7 +618,7 @@
         EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
             (fn (i, to_sbd) => EVERY' [rtac subsetI,
-              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
               rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
               etac set_rev_mp, REPEAT_DETERM o etac allE,
               etac (mk_conjunctN n i)])
@@ -623,7 +626,7 @@
       (Lev_Sucs ~~ to_sbdss)] 1
   end;
 
-fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
+fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
   let
     val n = length Lev_0s;
     val ks = n downto 1;
@@ -637,16 +640,17 @@
       CONJ_WRAP' (fn Lev_Suc =>
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
-              REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
+            (fn i =>
+              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+                rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
+                REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
       Lev_Sucs] 1
   end;
 
 fun mk_length_Lev'_tac length_Lev =
   EVERY' [ftac length_Lev, etac ssubst, atac] 1;
 
-fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
+fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
   let
     val n = length Lev_0s;
     val ks = n downto 1;
@@ -655,18 +659,21 @@
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn Lev_0 =>
         EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
-          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
-          hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
+          etac @{thm singletonE}, hyp_subst_tac ctxt,
+          dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
+          hyp_subst_tac ctxt,
+          rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
+            (fn i =>
+              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
+              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
               rtac Lev_0, rtac @{thm singletonI},
-              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
+              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
               rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
               rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
@@ -699,7 +706,7 @@
       ks)] 1
   end;
 
-fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
+fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
   let
     val n = length Lev_0s;
     val ks = 1 upto n;
@@ -718,7 +725,7 @@
         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, coalg_set)) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
               rtac (rv_Cons RS arg_cong RS iffD2),
               rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
               etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
@@ -728,7 +735,7 @@
       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
   end;
 
-fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
+fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   let
     val n = length Lev_0s;
     val ks = 1 upto n;
@@ -737,10 +744,10 @@
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
         EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
-          etac @{thm singletonE}, hyp_subst_tac,
+          etac @{thm singletonE}, hyp_subst_tac ctxt,
           CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
             (if i = i'
-            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
+            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
               CONJ_WRAP' (fn (i'', Lev_0'') =>
                 EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
                   rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
@@ -756,7 +763,7 @@
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, from_to_sbd) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
                 CONJ_WRAP' (fn i' => rtac impI THEN'
                   CONJ_WRAP' (fn i'' =>
                     EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
@@ -774,7 +781,7 @@
       ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
   end;
 
-fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
+fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
   let
     val n = length Lev_0s;
     val ks = 1 upto n;
@@ -783,18 +790,18 @@
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
         EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
-          etac @{thm singletonE}, hyp_subst_tac,
+          etac @{thm singletonE}, hyp_subst_tac ctxt,
           CONJ_WRAP' (fn i' => rtac impI THEN'
             CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
               (if i = i''
               then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
                 dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
-                hyp_subst_tac,
+                hyp_subst_tac ctxt,
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
                   (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
                     dtac list_inject_iffD1 THEN' etac conjE THEN'
                     (if k = i'
-                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
+                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
                     else etac (mk_InN_not_InM i' k RS notE)))
                 (rev ks)]
               else etac (mk_InN_not_InM i'' i RS notE)))
@@ -806,7 +813,7 @@
         EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, to_sbd_inj)) =>
-              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
+              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
               CONJ_WRAP' (fn i' => rtac impI THEN'
                 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
                 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
@@ -816,7 +823,7 @@
                   (if k = i
                   then EVERY' [dtac (mk_InN_inject n i),
                     dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
-                    atac, atac, hyp_subst_tac] THEN'
+                    atac, atac, hyp_subst_tac ctxt] THEN'
                     CONJ_WRAP' (fn i'' =>
                       EVERY' [rtac impI, dtac (sym RS trans),
                         rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
@@ -875,7 +882,7 @@
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
-                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
+                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
               (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
@@ -901,7 +908,7 @@
                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
                   REPEAT_DETERM_N 4 o etac thin_rl,
                   rtac set_image_Lev,
-                  atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
+                  atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
               (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
@@ -958,7 +965,7 @@
                 dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
                   dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
-                  atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
+                  atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
@@ -973,7 +980,7 @@
                 dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
                   dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
-                  atac, atac, hyp_subst_tac, atac]
+                  atac, atac, hyp_subst_tac ctxt, atac]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
@@ -1132,11 +1139,11 @@
     CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
       rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
 
-fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
+fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
     EVERY' (map2 (fn srel_mono => fn srel_Id =>
       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
-        etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
+        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
         REPEAT_DETERM_N m o rtac @{thm subset_refl},
         REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
         rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
@@ -1220,7 +1227,7 @@
         replicate n (@{thm o_id} RS fun_cong))))
     maps map_comps map_cong0s)] 1;
 
-fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
+fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
   set_hset_hsetsss =
   let
     val n = length map_comp's;
@@ -1230,8 +1237,8 @@
       coinduct_tac] @
       maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
         set_hset_hsetss) =>
-        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
-         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
+        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
+         rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
          REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
          rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
@@ -1309,7 +1316,7 @@
     @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
     ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
 
-fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
+fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
   sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
   let
     val n = length isNode_hsets;
@@ -1331,7 +1338,7 @@
       rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
       rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
       ftac (carT_def RS equalityD1 RS set_mp),
-      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
       rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
       rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
       rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
@@ -1371,7 +1378,7 @@
   CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
     EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
       REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
-      hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
+      hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
       EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
       pickWP_assms_tac,
       SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
@@ -1395,7 +1402,7 @@
       CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
         EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
-          hyp_subst_tac,
+          hyp_subst_tac ctxt,
           SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
           rtac (map_comp RS trans),
           SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
@@ -1412,7 +1419,7 @@
   CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
   CONJ_WRAP' (fn (unfold, map_comp) =>
     EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
-      hyp_subst_tac,
+      hyp_subst_tac ctxt,
       SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
       rtac refl])
   (unfolds ~~ map_comps) 1;
@@ -1431,7 +1438,7 @@
       CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
         EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
-          hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
+          hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
           EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
           pickWP_assms_tac,
           rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -1443,7 +1450,7 @@
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
             EVERY' [rtac @{thm UN_least},
               SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
-              etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
+              etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
               dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
           (ks ~~ rev (drop m set_maps))])
       (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
@@ -1484,18 +1491,18 @@
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
+          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
             K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
-  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
+  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
-  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
+  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
-fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
-  set_maps dtor_set_incls dtor_set_set_inclss =
+fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+    dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
   let
     val m = length dtor_set_incls;
     val n = length dtor_set_set_inclss;
@@ -1536,7 +1543,7 @@
                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
-                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_maps ~~ in_Jsrels))])
         (dtor_sets ~~ passive_set_maps),
         rtac conjI,
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -294,7 +294,7 @@
       in
         map2 (fn goal => fn alg_set =>
           Goal.prove_sorry lthy [] []
-            goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
+            goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
           |> Thm.close_derivation)
         goals alg_set_thms
       end;
@@ -420,7 +420,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
              (Logic.list_implies (prems, concl)))
-          (K ((hyp_subst_tac THEN' atac) 1))
+          (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
       end;
 
@@ -654,7 +654,7 @@
 
         val monos =
           map2 (fn goal => fn min_algs =>
-            Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
+            Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
             |> Thm.close_derivation)
           (map mk_mono_goal min_algss) min_algs_thms;
 
@@ -1315,7 +1315,7 @@
       in
         (Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (phis @ Izs) goal)
-          (K (mk_ctor_induct_tac m set_map'ss init_induct_thm morE_thms mor_Abs_thm
+          (K (mk_ctor_induct_tac lthy m set_map'ss init_induct_thm morE_thms mor_Abs_thm
             Rep_inverses Abs_inverses Reps))
         |> Thm.close_derivation,
         rev (Term.add_tfrees goal []))
@@ -1677,7 +1677,7 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
+              (K (mk_lfp_map_wpull_tac lthy m (rtac induct) map_wpulls ctor_map_thms
                 (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
               |> Thm.close_derivation;
           in
@@ -1728,13 +1728,14 @@
               ctors (0 upto n - 1) witss
           end;
 
-        fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
+        fun wit_tac ctxt _ = mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
           fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
               fn T => fn wits => fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b
-              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac lthy) (SOME deads)
+              map_b rel_b set_bs
+              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
               lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
@@ -1780,7 +1781,7 @@
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
               fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
+               (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
                  ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
diff -r 182454c06a80 -r ad3a241def73 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -10,7 +10,7 @@
 sig
   val mk_alg_min_alg_tac: int -> thm -> thm list -> thm -> thm -> thm list list -> thm list ->
     thm list -> tactic
-  val mk_alg_not_empty_tac: thm -> thm list -> thm list -> tactic
+  val mk_alg_not_empty_tac: Proof.context -> thm -> thm list -> thm list -> tactic
   val mk_alg_select_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_alg_set_tac: thm -> tactic
   val mk_bd_card_order_tac: thm list -> tactic
@@ -18,13 +18,13 @@
   val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
   val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic
   val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
-  val mk_ctor_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list ->
-    thm list -> tactic
+  val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
+    thm list -> thm list -> thm list -> tactic
   val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
-  val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
-    thm list -> thm list -> thm list list -> tactic
+  val mk_ctor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+    thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
   val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
@@ -38,8 +38,8 @@
   val mk_iso_alt_tac: thm list -> thm -> tactic
   val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
-  val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
-    thm list list list -> thm list -> tactic
+  val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
+    thm list list -> thm list list list -> thm list -> tactic
   val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
   val mk_map_id_tac: thm list -> thm -> tactic
   val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
@@ -49,7 +49,7 @@
   val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
     thm -> thm -> thm -> thm -> thm -> thm -> tactic
   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
-  val mk_min_algs_mono_tac: thm -> tactic
+  val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   val mk_min_algs_tac: thm -> thm list -> tactic
   val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
   val mk_mor_Rep_tac: thm list -> thm -> thm list -> thm list -> thm list ->
@@ -73,7 +73,7 @@
     thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
   val mk_set_map_tac: thm -> tactic
   val mk_set_tac: thm -> tactic
-  val mk_wit_tac: int -> thm list -> thm list -> tactic
+  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
   val mk_wpull_tac: thm -> tactic
 end;
 
@@ -95,13 +95,13 @@
   EVERY' [etac bspec, rtac CollectI] 1 THEN
   REPEAT_DETERM (etac conjI 1) THEN atac 1;
 
-fun mk_alg_not_empty_tac alg_set alg_sets wits =
-  (EVERY' [rtac notI, hyp_subst_tac, ftac alg_set] THEN'
+fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
+  (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
   REPEAT_DETERM o FIRST'
     [rtac subset_UNIV,
     EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
     EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
-    EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac,
+    EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
       FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
   etac @{thm emptyE}) 1;
 
@@ -280,10 +280,10 @@
     CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
   end;
 
-fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
+fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
   rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2},
   rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac,
-  rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac, rtac refl] 1;
+  rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
 
 fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
@@ -384,7 +384,7 @@
     REPEAT_DETERM o etac conjE, atac] 1;
 
 fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
-  EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
+  EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN
   unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
 
 fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
@@ -531,7 +531,7 @@
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
   etac fold_unique_mor 1;
 
-fun mk_ctor_induct_tac m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
+fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   let
     val n = length set_map'ss;
     val ks = 1 upto n;
@@ -539,7 +539,7 @@
     fun mk_IH_tac Rep_inv Abs_inv set_map' =
       DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
         dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE,
-        hyp_subst_tac, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
+        hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
 
     fun mk_closed_tac (k, (morE, set_map's)) =
       EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
@@ -680,7 +680,7 @@
     (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
   end;
 
-fun mk_lfp_map_wpull_tac m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
+fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
   let
     val n = length wpulls;
     val ks = 1 upto n;
@@ -718,7 +718,7 @@
           CONJ_WRAP' (K (rtac subset_refl)) ks,
         rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
         rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
-        hyp_subst_tac, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
+        hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
         CONJ_WRAP' mk_subset ctor_sets];
   in
     (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1
@@ -763,7 +763,7 @@
   EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
     rtac wpull, REPEAT_DETERM o atac] 1;
 
-fun mk_wit_tac n ctor_set wit =
+fun mk_wit_tac ctxt n ctor_set wit =
   REPEAT_DETERM (atac 1 ORELSE
     EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
     REPEAT_DETERM o
@@ -771,10 +771,10 @@
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
+          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_srel_tac ctxt in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
   ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
   let
     val m = length ctor_set_incls;
@@ -821,7 +821,7 @@
                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
-                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_maps ~~ in_Isrels))])
         (ctor_sets ~~ passive_set_maps),
         rtac conjI,
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Bali/AxSem.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -693,7 +693,7 @@
 apply       (tactic "ALLGOALS strip_tac")
 apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
          etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
-apply       (tactic "TRYALL hyp_subst_tac")
+apply       (tactic "TRYALL (hyp_subst_tac @{context})")
 apply       (simp, rule ax_derivs.empty)
 apply      (drule subset_insertD)
 apply      (blast intro: ax_derivs.insert)
diff -r 182454c06a80 -r ad3a241def73 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/HOL.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -849,15 +849,15 @@
 let
   fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
     | non_bool_eq _ = false;
-  val hyp_subst_tac' =
+  fun hyp_subst_tac' ctxt =
     SUBGOAL (fn (goal, i) =>
       if Term.exists_Const non_bool_eq goal
-      then Hypsubst.hyp_subst_tac i
+      then Hypsubst.hyp_subst_tac ctxt i
       else no_tac);
 in
   Hypsubst.hypsubst_setup
   (*prevent substitution on bool*)
-  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
 end
 *}
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -1082,7 +1082,7 @@
 
 fun Seq_case_tac ctxt s i =
   res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
-  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
 
 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
 fun Seq_case_simp_tac ctxt s i =
@@ -1103,7 +1103,7 @@
 
 fun pair_tac ctxt s =
   res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
-  THEN' hyp_subst_tac THEN' asm_full_simp_tac ctxt;
+  THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
 
 (* induction on a sequence of pairs with pairsplitting and simplification *)
 fun pair_induct_tac ctxt s rws i =
diff -r 182454c06a80 -r ad3a241def73 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -201,7 +201,7 @@
 apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
 apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
   THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
-apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
+apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac @{context}])")
 
 -- "Level 7"
 -- "15 NewC"
@@ -240,7 +240,7 @@
 
 -- "for FAss"
 apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
-       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
+       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
 
 -- "for if"
 apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -1738,7 +1738,7 @@
                rotate_tac ~1 1,
                ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
                   (put_simpset HOL_ss context addsimps flat distinct_thms)) 1] @
-               (if null idxs then [] else [hyp_subst_tac 1,
+               (if null idxs then [] else [hyp_subst_tac context 1,
                 SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
                   let
                     val SOME prem = find_first (can (HOLogic.dest_eq o
diff -r 182454c06a80 -r ad3a241def73 src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -536,11 +536,11 @@
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 method_setup valid_certificate_tac = {*
-  Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
+  Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
     (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
              assume_tac i,
-             etac conjE i, REPEAT (hyp_subst_tac i)])))
+             etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
 
 text{*The @{text "(no_asm)"} attribute is essential, since it retains
diff -r 182454c06a80 -r ad3a241def73 src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/SET_Protocol/Purchase.thy	Sat Apr 27 20:50:20 2013 +0200
@@ -481,9 +481,9 @@
 
 method_setup valid_certificate_tac = {*
   Args.goal_spec >> (fn quant =>
-    K (SIMPLE_METHOD'' quant (fn i =>
+    fn ctxt => SIMPLE_METHOD'' quant (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
-             assume_tac i, REPEAT (hyp_subst_tac i)])))
+             assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
 
 
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -418,13 +418,13 @@
         val inj_thm =
           Goal.prove_sorry_global thy5 [] []
             (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
-            (fn _ => EVERY
+            (fn {context = ctxt, ...} => EVERY
               [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
                REPEAT (EVERY
                  [rtac allI 1, rtac impI 1,
                   Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
                   REPEAT (EVERY
-                    [hyp_subst_tac 1,
+                    [hyp_subst_tac ctxt 1,
                      rewrite_goals_tac rewrites,
                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
                      (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
@@ -480,7 +480,7 @@
       if length descr = 1 then []
       else
         drop (length newTs) (Datatype_Aux.split_conj_thm
-          (Goal.prove_sorry_global thy5 [] [] iso_t (fn _ => EVERY
+          (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
              [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
               REPEAT (rtac TrueI 1),
               rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
@@ -489,7 +489,7 @@
               REPEAT (EVERY
                 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
                    maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
-                 TRY (hyp_subst_tac 1),
+                 TRY (hyp_subst_tac ctxt 1),
                  rtac (sym RS range_eqI) 1,
                  resolve_tac iso_char_thms 1])])));
 
@@ -556,9 +556,9 @@
                Lim_inject, Suml_inject, Sumr_inject])
       in
         Goal.prove_sorry_global thy5 [] [] t
-          (fn _ => EVERY
+          (fn {context = ctxt, ...} => EVERY
             [rtac iffI 1,
-             REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
+             REPEAT (etac conjE 2), hyp_subst_tac ctxt 2, rtac refl 2,
              dresolve_tac rep_congs 1, dtac box_equals 1,
              REPEAT (resolve_tac rep_thms 1),
              REPEAT (eresolve_tac inj_thms 1),
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -179,9 +179,9 @@
                 etac elim 1,
                 REPEAT_DETERM_N j distinct_tac,
                 TRY (dresolve_tac inject 1),
-                REPEAT (etac conjE 1), hyp_subst_tac 1,
+                REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
                 REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
-                TRY (hyp_subst_tac 1),
+                TRY (hyp_subst_tac ctxt 1),
                 rtac refl 1,
                 REPEAT_DETERM_N (n - j - 1) distinct_tac],
               intrs, j + 1)
@@ -403,14 +403,15 @@
     fun prove_nchotomy (t, exhaustion) =
       let
         (* For goal i, select the correct disjunct to attack, then prove it *)
-        fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
-          | tac i n = rtac disjI2 i THEN tac i (n - 1);
+        fun tac ctxt i 0 =
+              EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
+          | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
       in
         Goal.prove_sorry_global thy [] [] t
-          (fn _ =>
+          (fn {context = ctxt, ...} =>
             EVERY [rtac allI 1,
              Datatype_Aux.exh_tac (K exhaustion) 1,
-             ALLGOALS (fn i => tac i (i - 1))])
+             ALLGOALS (fn i => tac ctxt i (i - 1))])
       end;
 
     val nchotomys =
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -534,7 +534,7 @@
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
 
 fun simp_case_tac ctxt i =
-  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac] i;
+  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
 
 in
 
@@ -724,7 +724,7 @@
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
+         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
diff -r 182454c06a80 -r ad3a241def73 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -317,7 +317,7 @@
 fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
   THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
   THEN' REPEAT_DETERM o etac @{thm conjE}
-  THEN' TRY o hyp_subst_tac' ctxt;
+  THEN' TRY o hyp_subst_tac ctxt;
 
 fun intro_image_tac ctxt = rtac @{thm image_eqI}
     THEN' (REPEAT_DETERM1 o
@@ -332,7 +332,7 @@
   THEN' REPEAT_DETERM o CHANGED o
     (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
     THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-    THEN' TRY o hyp_subst_tac' ctxt)
+    THEN' TRY o hyp_subst_tac ctxt)
 
 fun tac1_of_formula ctxt (Int (fm1, fm2)) =
     TRY o etac @{thm conjE}
@@ -376,16 +376,16 @@
        ORELSE' etac @{thm conjE}
        ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
          TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
-         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})
+         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
        ORELSE' (etac @{thm imageE}
          THEN' (REPEAT_DETERM o CHANGED o
          (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
          THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-         THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl})))
+         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
        ORELSE' etac @{thm ComplE}
        ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
         THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
-        THEN' TRY o hyp_subst_tac' ctxt THEN' TRY o rtac @{thm refl}))
+        THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
 
 fun tac ctxt fm =
   let
@@ -398,7 +398,7 @@
       THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
       THEN' REPEAT_DETERM o resolve_tac @{thms exI}
       THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
-      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac' ctxt) THEN' rtac @{thm refl}))))
+      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
       THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
         REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
   in
diff -r 182454c06a80 -r ad3a241def73 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Provers/classical.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -25,8 +25,8 @@
   val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
   val classical: thm  (* (~ P ==> P) ==> P *)
   val sizef: thm -> int  (* size function for BEST_FIRST, typically size_of_thm *)
-  val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
-    the hypotheses; assumed to be safe! *)
+  val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for
+    substitution in the hypotheses; assumed to be safe! *)
 end;
 
 signature BASIC_CLASSICAL =
@@ -697,7 +697,7 @@
        [eq_assume_tac,
         eq_mp_tac,
         bimatch_from_nets_tac safe0_netpair,
-        FIRST' Data.hyp_subst_tacs,
+        FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
         bimatch_from_nets_tac safep_netpair])
   end;
 
@@ -733,7 +733,7 @@
      (FIRST'
        [eq_assume_contr_tac,
         bimatch_from_nets_tac safe0_netpair,
-        FIRST' Data.hyp_subst_tacs,
+        FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
         n_bimatch_from_nets_tac 1 safep_netpair,
         bimatch2_tac safep_netpair])
   end;
diff -r 182454c06a80 -r ad3a241def73 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Provers/hypsubst.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -46,9 +46,8 @@
 
 signature HYPSUBST =
 sig
-  val bound_hyp_subst_tac    : int -> tactic
-  val hyp_subst_tac          : int -> tactic
-  val hyp_subst_tac'         : Proof.context -> int -> tactic
+  val bound_hyp_subst_tac    : Proof.context -> int -> tactic
+  val hyp_subst_tac          : Proof.context -> int -> tactic
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
@@ -127,14 +126,10 @@
 
   (*Select a suitable equality assumption; substitute throughout the subgoal
     If bnd is true, then it replaces Bound variables only. *)
-  fun gen_hyp_subst_tac opt_ctxt bnd =
+  fun gen_hyp_subst_tac ctxt bnd =
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
         val (k, _) = eq_var bnd true Bi
-        val ctxt =
-          (case opt_ctxt of
-            NONE => Proof_Context.init_global (Thm.theory_of_thm st)
-          | SOME ctxt => ctxt)
         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
         etac thin_rl i, rotate_tac (~k) i]
@@ -198,15 +193,13 @@
       handle THM _ => no_tac | EQ_VAR => no_tac);
 
 (*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
-
-fun hyp_subst_tac' ctxt = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac (SOME ctxt) false, vars_gen_hyp_subst_tac false];
+fun hyp_subst_tac ctxt =
+  FIRST' [ematch_tac [Data.thin_refl],
+    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
 
 (*Substitutes for Bound variables only -- this is always safe*)
-val bound_hyp_subst_tac =
-    gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
+fun bound_hyp_subst_tac ctxt =
+  gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
 
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are
@@ -271,7 +264,7 @@
 
 val hypsubst_setup =
   Method.setup @{binding hypsubst}
-    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
+    (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
     "substitution using an assumption (improper)" #>
   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
     "simple substitution";
diff -r 182454c06a80 -r ad3a241def73 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -14,8 +14,8 @@
   val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
   val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
   val print_rules: Proof.context -> unit
-  val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
-  val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
+  val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
+  val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
   val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
   val wrap: Proof.context -> (int -> tactic) -> int -> tactic
   val intro_bang: int option -> attribute
@@ -68,8 +68,9 @@
  {next: int,
   rules: (int * ((int * bool) * thm)) list,
   netpairs: netpair list,
-  wrappers: (((int -> tactic) -> int -> tactic) * stamp) list *
-    (((int -> tactic) -> int -> tactic) * stamp) list};
+  wrappers:
+    ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
+    ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list};
 
 fun make_rules next rules netpairs wrappers =
   Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
@@ -170,7 +171,7 @@
 
 fun gen_wrap which ctxt =
   let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
-  in fold_rev fst (which wrappers) end;
+  in fold_rev (fn (w, _) => w ctxt) (which wrappers) end;
 
 val Swrap = gen_wrap #1;
 val wrap = gen_wrap #2;
diff -r 182454c06a80 -r ad3a241def73 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -231,7 +231,7 @@
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
                         ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
                                               type_elims)
-                        ORELSE' hyp_subst_tac)),
+                        ORELSE' hyp_subst_tac ctxt1)),
      if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
      else all_tac,
      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
@@ -254,7 +254,7 @@
   (*Breaks down logical connectives in the monotonic function*)
   val basic_elim_tac =
       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
-                ORELSE' bound_hyp_subst_tac))
+                ORELSE' bound_hyp_subst_tac ctxt1))
       THEN prune_params_tac
           (*Mutual recursion: collapse references to Part(D,h)*)
       THEN (PRIMITIVE (fold_rule part_rec_defs));
@@ -348,7 +348,7 @@
             (*Now break down the individual cases.  No disjE here in case
               some premise involves disjunction.*)
             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
-                               ORELSE' bound_hyp_subst_tac)),
+                               ORELSE' (bound_hyp_subst_tac ctxt1))),
             ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
 
      val dummy =