# HG changeset patch
# User wenzelm
# Date 1213478391 -7200
# Node ID 5fe899199f85509bd1e4cb085f8f03ec26e10cd6
# Parent  548e2d3105b9f0a6e31255cbe12e3580b3013842
proper context for tactics derived from res_inst_tac;

diff -r 548e2d3105b9 -r 5fe899199f85 doc-src/IsarRef/Thy/ML_Tactic.thy
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -41,7 +41,7 @@
   @{ML forward_tac}).
 
   \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
-  @{ML res_inst_tac}).
+  @{ML RuleInsts.res_inst_tac}).
 
   \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
   vs.\ @{ML rtac}).
@@ -66,11 +66,11 @@
   \begin{tabular}{lll}
     @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
     @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
-    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
+    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
     @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
     @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
     @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
-    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
+    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
     @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
   \end{tabular}
   \medskip
diff -r 548e2d3105b9 -r 5fe899199f85 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/CCL.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -414,7 +414,8 @@
   done
 
 ML {*
-  fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
+  fun po_coinduct_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
 *}
 
 
@@ -459,8 +460,11 @@
   done
 
 ML {*
-  fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
-  fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
+  fun eq_coinduct_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
+
+  fun eq_coinduct3_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
 *}
 
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/Hered.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -97,7 +97,8 @@
   done
 
 ML {*
-  fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
+  fun HTT_coinduct_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
 *}
 
 lemma HTT_coinduct3:
@@ -109,7 +110,8 @@
 ML {*
 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
 
-fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
+fun HTT_coinduct3_tac ctxt s i =
+  RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
 
 val HTTgenIs =
   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
diff -r 548e2d3105b9 -r 5fe899199f85 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/Wfd.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -54,8 +54,8 @@
   done
 
 ML {*
-  fun wfd_strengthen_tac s i =
-    res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
+  fun wfd_strengthen_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
 *}
 
 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
@@ -123,7 +123,7 @@
   shows "Wfd(R**S)"
   apply (unfold Wfd_def)
   apply safe
-  apply (tactic {* wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1 *})
+  apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
    apply (blast elim!: lex_pair)
   apply (subgoal_tac "ALL a b.<a,b>:P")
    apply blast
@@ -209,7 +209,7 @@
 lemma NatPR_wf: "Wfd(NatPR)"
   apply (unfold Wfd_def)
   apply clarify
-  apply (tactic {* wfd_strengthen_tac "%x. x:Nat" 1 *})
+  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
    apply (fastsimp iff: NatPRXH)
   apply (erule Nat_ind)
    apply (fastsimp iff: NatPRXH)+
@@ -218,7 +218,7 @@
 lemma ListPR_wf: "Wfd(ListPR(A))"
   apply (unfold Wfd_def)
   apply clarify
-  apply (tactic {* wfd_strengthen_tac "%x. x:List (A)" 1 *})
+  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
    apply (fastsimp iff: ListPRXH)
   apply (erule List_ind)
    apply (fastsimp iff: ListPRXH)+
@@ -465,7 +465,7 @@
        | _ => false
 in
 
-fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i
+fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i
                        in IHinst tac rcallTs i end THEN
                   eresolve_tac rcall_lemmas i
 
@@ -487,7 +487,7 @@
                                  hyp_subst_tac)
 
 val clean_ccs_tac =
-       let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i
+       let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i
        in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
                        eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
                        hyp_subst_tac)) end
diff -r 548e2d3105b9 -r 5fe899199f85 src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/ex/Stream.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -32,7 +32,7 @@
 lemma map_comp:
   assumes 1: "l:Lists(A)"
   shows "map(f o g,l) = map(f,map(g,l))"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
    apply (blast intro: 1)
   apply safe
@@ -46,7 +46,7 @@
 lemma map_id:
   assumes 1: "l:Lists(A)"
   shows "map(%x. x,l) = l"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
   apply (blast intro: 1)
   apply safe
@@ -62,7 +62,7 @@
   assumes "l:Lists(A)"
     and "m:Lists(A)"
   shows "map(f,l@m) = map(f,l) @ map(f,m)"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
   apply (blast intro: prems)
   apply safe
@@ -81,7 +81,7 @@
     and "l:Lists(A)"
     and "m:Lists(A)"
   shows "k @ l @ m = (k @ l) @ m"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
   apply (blast intro: prems)
   apply safe
@@ -99,7 +99,7 @@
 lemma ilist_append:
   assumes "l:ILists(A)"
   shows "l @ m = l"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
   apply (blast intro: prems)
   apply safe
@@ -133,7 +133,7 @@
   done
 
 lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
-  apply (tactic {* eq_coinduct3_tac
+  apply (tactic {* eq_coinduct3_tac @{context}
     "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
   apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
   apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
diff -r 548e2d3105b9 -r 5fe899199f85 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/Arith.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -130,7 +130,7 @@
 
 lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
 apply (unfold arith_defs)
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
 apply (tactic "hyp_rew_tac []")
 done
 
@@ -140,7 +140,7 @@
 lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
 apply (unfold arith_defs)
 apply (tactic "hyp_rew_tac []")
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
 apply (tactic "hyp_rew_tac []")
 done
 
@@ -188,7 +188,7 @@
 
 (*Associative law for addition*)
 lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic "hyp_arith_rew_tac []")
 done
 
@@ -196,11 +196,11 @@
 (*Commutative law for addition.  Can be proved using three inductions.
   Must simplify after first induction!  Orientation of rewrites is delicate*)
 lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic "hyp_arith_rew_tac []")
-apply (tactic {* NE_tac "b" 2 *})
+apply (tactic {* NE_tac @{context} "b" 2 *})
 apply (rule sym_elem)
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
 apply (tactic "hyp_arith_rew_tac []")
 done
 
@@ -209,33 +209,33 @@
 
 (*right annihilation in product*)
 lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic "hyp_arith_rew_tac []")
 done
 
 (*right successor law for multiplication*)
 lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
-apply (tactic {* NE_tac "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
 done
 
 (*Commutative law for multiplication*)
 lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
-apply (tactic {* NE_tac "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *})
 done
 
 (*addition distributes over multiplication*)
 lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
-apply (tactic {* NE_tac "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
 done
 
 (*Associative law for multiplication*)
 lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
-apply (tactic {* NE_tac "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
 done
 
 
@@ -246,7 +246,7 @@
   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
 
 lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic "hyp_arith_rew_tac []")
 done
 
@@ -258,12 +258,12 @@
   An example of induction over a quantified formula (a product).
   Uses rewriting with a quantified, implicative inductive hypothesis.*)
 lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
 (*strip one "universal quantifier" but not the "implication"*)
 apply (rule_tac [3] intr_rls)
 (*case analysis on x in
     (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
+apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4")
 (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
 apply (rule_tac [5] replace_type)
 apply (rule_tac [4] replace_type)
@@ -326,7 +326,7 @@
 
 (*If a+b=0 then a=0.   Surprisingly tedious*)
 lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (rule_tac [3] replace_type)
 apply (tactic "arith_rew_tac []")
 apply (tactic "intr_tac []") (*strips remaining PRODs*)
@@ -434,14 +434,14 @@
      succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
 apply (rule divC_succ [THEN trans_elem])
 apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
-apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
+apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
 apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
 done
 
 (*for case analysis on whether a number is 0 or a successor*)
 lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
                       Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (rule_tac [3] PlusI_inr)
 apply (rule_tac [2] PlusI_inl)
 apply (tactic eqintr_tac)
@@ -450,7 +450,7 @@
 
 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
 lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
 apply (rule EqE)
diff -r 548e2d3105b9 -r 5fe899199f85 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/CTT.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -354,29 +354,25 @@
 
 ML {*
 local
-  val routine_rls = thms "routine_rls";
-  val form_rls = thms "form_rls";
-  val intr_rls = thms "intr_rls";
-  val element_rls = thms "element_rls";
-  val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
-    thms "elimL_rls" @ thms "refl_elem"
+  val equal_rls = @{thms form_rls} @ @{thms element_rls} @ @{thms intrL_rls} @
+    @{thms elimL_rls} @ @{thms refl_elem}
 in
 
 fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
 
 (*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
+val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1));
 
 (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
 fun typechk_tac thms =
-  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
+  let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
   in  REPEAT_FIRST (ASSUME tac)  end
 
 (*Solve a:A (a flexible, A rigid) by introduction rules.
   Cannot use stringtrees (filt_resolve_tac) since
   goals like ?a:SUM(A,B) have a trivial head-string *)
 fun intr_tac thms =
-  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
+  let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
   in  REPEAT_FIRST (ASSUME tac)  end
 
 (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
@@ -412,55 +408,40 @@
 lemmas reduction_rls = comp_rls [THEN trans_elem]
 
 ML {*
-local
-  val EqI = thm "EqI";
-  val EqE = thm "EqE";
-  val NE = thm "NE";
-  val FE = thm "FE";
-  val ProdI = thm "ProdI";
-  val SumI = thm "SumI";
-  val SumE = thm "SumE";
-  val PlusE = thm "PlusE";
-  val PlusI_inl = thm "PlusI_inl";
-  val PlusI_inr = thm "PlusI_inr";
-  val subst_prodE = thm "subst_prodE";
-  val intr_rls = thms "intr_rls";
-in
-
 (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1))
+val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
 
 (** Tactics that instantiate CTT-rules.
     Vars in the given terms will be incremented!
     The (rtac EqE i) lets them apply to equality judgements. **)
 
-fun NE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
+fun NE_tac ctxt sp i =
+  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
 
-fun SumE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
+fun SumE_tac ctxt sp i =
+  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
 
-fun PlusE_tac (sp: string) i =
-  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
+fun PlusE_tac ctxt sp i =
+  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
 
 (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
 
 (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
 fun add_mp_tac i =
-    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i
+    rtac @{thm subst_prodE} i  THEN  assume_tac i  THEN  assume_tac i
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = etac subst_prodE i  THEN  assume_tac i
+fun mp_tac i = etac @{thm subst_prodE} i  THEN  assume_tac i
 
 (*"safe" when regarded as predicate calculus rules*)
 val safe_brls = sort (make_ord lessb)
-    [ (true,FE), (true,asm_rl),
-      (false,ProdI), (true,SumE), (true,PlusE) ]
+    [ (true, @{thm FE}), (true,asm_rl),
+      (false, @{thm ProdI}), (true, @{thm SumE}), (true, @{thm PlusE}) ]
 
 val unsafe_brls =
-    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
-      (true,subst_prodE) ]
+    [ (false, @{thm PlusI_inl}), (false, @{thm PlusI_inr}), (false, @{thm SumI}),
+      (true, @{thm subst_prodE}) ]
 
 (*0 subgoals vs 1 or more*)
 val (safe0_brls, safep_brls) =
@@ -478,8 +459,6 @@
 
 (*Fails unless it solves the goal!*)
 fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
-
-end
 *}
 
 use "rew.ML"
diff -r 548e2d3105b9 -r 5fe899199f85 src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/ex/Equality.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -40,7 +40,7 @@
 lemma "[| a:N;  b:N;  c:N |]
       ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
           rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (tactic "hyp_rew_tac []")
 done
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/Bali/WellType.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -652,9 +652,13 @@
 apply (simp_all (no_asm_use) split del: split_if_asm)
 apply (safe del: disjE)
 (* 17 subgoals *)
-apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
+apply (tactic {* ALLGOALS (fn i =>
+  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
+    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
+    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
+  else RuleInsts.thin_tac @{context} "All ?P" i) *})
 (*apply (safe del: disjE elim!: wt_elim_cases)*)
-apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
+apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
 apply (simp_all (no_asm_use) split del: split_if_asm)
 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
 apply ((blast del: equalityCE dest: sym [THEN trans])+)
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/IMPP/Hoare.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -282,7 +282,9 @@
 apply          (blast) (* asm *)
 apply         (blast) (* cut *)
 apply        (blast) (* weaken *)
-apply       (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *})
+apply       (tactic {* ALLGOALS (EVERY'
+  [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
+   simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
 apply       (simp_all (no_asm_use) add: triple_valid_def2)
 apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
 apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -107,9 +107,9 @@
 apply (tactic "split_all_tac 1", rename_tac P e Q)
 apply (rule hoare_ehoare.induct)
 (*18*)
-apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
-apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *})
-apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
+apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
 apply (simp_all only: cnvalid1_eq cenvalid_def2)
                  apply fast
                 apply fast
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -762,12 +762,14 @@
    steps of the implementation, and try to solve the idling case by simplification
 *)
 ML {*
-fun split_idle_tac ss simps i =
-  TRY (rtac @{thm actionI} i) THEN
-  case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
-  rewrite_goals_tac @{thms action_rews} THEN
-  forward_tac [temp_use @{thm Step1_4_7}] i THEN
-  asm_full_simp_tac (ss addsimps simps) i
+fun split_idle_tac ctxt simps i =
+  let val ss = Simplifier.local_simpset_of ctxt in
+    TRY (rtac @{thm actionI} i) THEN
+    InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
+    rewrite_goals_tac @{thms action_rews} THEN
+    forward_tac [temp_use @{thm Step1_4_7}] i THEN
+    asm_full_simp_tac (ss addsimps simps) i
+  end
 *}
 (* ----------------------------------------------------------------------
    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
@@ -779,7 +781,7 @@
 lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
              --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
-  apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
+  apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
   apply force
   done
 (* turn into (unsafe, looping!) introduction rule *)
@@ -851,7 +853,7 @@
 
 lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S1 rmhist p)$ | (S2 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_1 [temp_use])
   done
 
@@ -885,7 +887,7 @@
 
 lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S2 rmhist p)$ | (S3 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_2 [temp_use])
   done
 
@@ -911,7 +913,7 @@
 
 lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_3 [temp_use])
   done
 
@@ -939,7 +941,7 @@
 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
         & (ALL l. $MemInv mm l)
         --> (S4 rmhist p)$ | (S5 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
@@ -949,7 +951,7 @@
          & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
          --> (S4 rmhist p & ires!p = #NotAResult)$
              | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
-  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
+  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
@@ -980,7 +982,7 @@
 lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
          --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
-  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
+  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   done
 
@@ -1009,7 +1011,7 @@
 
 lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S5 rmhist p)$ | (S6 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_5 [temp_use])
   done
 
@@ -1035,7 +1037,7 @@
 
 lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto dest!: Step1_2_6 [temp_use])
   done
 
@@ -1250,7 +1252,7 @@
   apply clarsimp
   apply (drule WriteS4 [action_use])
    apply assumption
-  apply (tactic "split_idle_tac @{simpset} [] 1")
+  apply (tactic "split_idle_tac @{context} [] 1")
   apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
     S4RPCUnch [temp_use])
      apply (auto simp: square_def dest: S4Write [temp_use])
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/TLA/TLA.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -305,17 +305,17 @@
 fun merge_box_tac i =
    REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
 
-fun merge_temp_box_tac i =
+fun merge_temp_box_tac ctxt i =
    REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
-                         eres_inst_tac [("'a","behavior")] @{thm box_thin} i])
+                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
 
-fun merge_stp_box_tac i =
+fun merge_stp_box_tac ctxt i =
    REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
-                         eres_inst_tac [("'a","state")] @{thm box_thin} i])
+                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
 
-fun merge_act_box_tac i =
+fun merge_act_box_tac ctxt i =
    REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
-                         eres_inst_tac [("'a","state * state")] @{thm box_thin} i])
+                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
 *}
 
 (* rewrite rule to push universal quantification through box:
@@ -947,7 +947,7 @@
   apply (clarsimp dest!: BoxSFI [temp_use])
   apply (erule (2) ensures [temp_use])
   apply (erule_tac F = F in dup_boxE)
-  apply (tactic "merge_temp_box_tac 1")
+  apply (tactic "merge_temp_box_tac @{context} 1")
   apply (erule STL4Edup)
   apply assumption
   apply (clarsimp simp: SF_def)
@@ -966,7 +966,7 @@
   apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
     simp: WF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
-  apply (tactic "merge_temp_box_tac 1")
+  apply (tactic "merge_temp_box_tac @{context} 1")
   apply (erule STL4Edup)
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -975,7 +975,7 @@
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
-  apply (tactic "merge_act_box_tac 1")
+  apply (tactic "merge_act_box_tac @{context} 1")
   apply (frule 4 [temp_use])
      apply assumption+
   apply (drule STL6 [temp_use])
@@ -984,7 +984,7 @@
   apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   apply (drule BoxWFI [temp_use])
   apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
-  apply (tactic "merge_temp_box_tac 1")
+  apply (tactic "merge_temp_box_tac @{context} 1")
   apply (erule DmdImpldup)
    apply assumption
   apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1004,7 +1004,7 @@
   apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
   apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
-  apply (tactic "merge_temp_box_tac 1")
+  apply (tactic "merge_temp_box_tac @{context} 1")
   apply (erule STL4Edup)
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -1013,14 +1013,14 @@
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
-  apply (tactic "merge_act_box_tac 1")
+  apply (tactic "merge_act_box_tac @{context} 1")
   apply (frule 4 [temp_use])
      apply assumption+
   apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   apply (drule BoxSFI [temp_use])
   apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
   apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
-  apply (tactic "merge_temp_box_tac 1")
+  apply (tactic "merge_temp_box_tac @{context} 1")
   apply (erule DmdImpldup)
    apply assumption
   apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -15,7 +15,7 @@
 sig
   include BASIC_SPLIT_RULE
   val split_rule_var: term -> thm -> thm
-  val split_rule_goal: string list list -> thm -> thm
+  val split_rule_goal: Proof.context -> string list list -> thm -> thm
   val setup: theory -> theory
 end;
 
@@ -123,14 +123,16 @@
   end;
 
 
-fun pair_tac s =
-  EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
+fun pair_tac ctxt s =
+  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+  THEN' hyp_subst_tac
+  THEN' K prune_params_tac;
 
 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
 
-fun split_rule_goal xss rl =
+fun split_rule_goal ctxt xss rl =
   let
-    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
+    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   in
     rl
@@ -148,7 +150,8 @@
   (Scan.lift (Args.parens (Args.$$$ "complete"))
     >> K (Thm.rule_attribute (K complete_split_rule)) ||
   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
-    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss))));
+    >> (fn xss => Thm.rule_attribute (fn context =>
+        split_rule_goal (Context.proof_of context) xss)));
 
 val setup =
   Attrib.add_attributes
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -41,8 +41,10 @@
                                     @{thm EnsuresI}, @{thm ensuresI}] 1),
               (*now there are two subgoals: co & transient*)
               simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
-              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
-              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
+              RuleInsts.res_inst_tac (Simplifier.the_context ss)
+                [(("act", 0), sact)] @{thm totalize_transientI} 2
+              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
+                [(("act", 0), sact)] @{thm transientI} 2,
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [@{thm Domain_def}]) 3,
               constrains_tac (cs,ss) 1,
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -104,7 +104,7 @@
   --> is_exec_frag A (cex_abs h (s,xs))"
 apply (unfold cex_abs_def)
 apply simp
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 txt {* main case *}
 apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
 done
@@ -204,7 +204,7 @@
          ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
 apply (unfold cex_abs_def mk_trace_def filter_act_def)
 apply simp
-apply (tactic {* pair_induct_tac "xs" [] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
 done
 
 
@@ -220,13 +220,13 @@
 apply (rule_tac x = "cex_abs h ex" in exI)
 apply auto
   (* Traces coincide *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (rule traces_coincide_abs)
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
 
   (* cex_abs is execution *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -237,7 +237,7 @@
 
  (* Liveness *)
 apply (simp add: temp_weakening_def2)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
 done
 
 (* FIX: NAch Traces.ML bringen *)
@@ -354,25 +354,25 @@
 
 (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
 lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
-apply (tactic {* Seq_case_simp_tac "x" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
 done
 
 lemma ex2seqConc [rule_format]:
 "Finite s1 -->
   (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
 apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac 1 *})
+apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
 apply blast
 (* main case *)
 apply clarify
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
 (* UU case *)
 apply (simp add: nil_is_Conc)
 (* nil case *)
 apply (simp add: nil_is_Conc)
 (* cons case *)
-apply (tactic {* pair_tac "aa" 1 *})
+apply (tactic {* pair_tac @{context} "aa" 1 *})
 apply auto
 done
 
@@ -390,11 +390,11 @@
 (* FIX: NAch Sequence.ML bringen *)
 
 lemma Mapnil: "(Map f$s = nil) = (s=nil)"
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 done
 
 lemma MapUU: "(Map f$s = UU) = (s=UU)"
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 done
 
 
@@ -432,9 +432,9 @@
 apply (unfold temp_strengthening_def state_strengthening_def
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 
@@ -442,25 +442,25 @@
 
 lemma TL_ex2seq_UU:
 "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 lemma TL_ex2seq_nil:
 "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 (* FIX: put to Sequence Lemmas *)
 lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
-apply (tactic {* Seq_induct_tac "s" [] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
 done
 
 (* important property of cex_absSeq: As it is a 1to1 correspondence,
@@ -475,19 +475,19 @@
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
 lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 apply auto
 done
 
 
 lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 
@@ -518,9 +518,9 @@
 apply (simp add: temp_weakening_def2 state_weakening_def2
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -216,7 +216,7 @@
        -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
             is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
 
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply (auto simp add: trans_of_defs2)
 done
@@ -230,7 +230,8 @@
        --> stutter (asig_of A) (fst s,ProjA2$xs)  &
            stutter (asig_of B) (snd s,ProjB2$xs)"
 
-apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs"
+  [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply (auto simp add: trans_of_defs2)
 done
@@ -243,8 +244,8 @@
 lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
    --> Forall (%x. fst x:act (A||B)) xs)"
 
-apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
-  thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+  @{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply auto
 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -263,8 +264,8 @@
      Forall (%x. fst x:act (A||B)) xs
      --> is_exec_frag (A||B) (s,xs)"
 
-apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
-  thm "is_exec_frag_def", thm "stutter_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+  @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
 apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
 done
 
@@ -279,7 +280,7 @@
   Forall (%x. fst x:act (A||B)) (snd ex))"
 
 apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
 apply (rule iffI)
 (* ==>  *)
 apply (erule conjE)+
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -219,7 +219,7 @@
 lemma lemma_2_1b:
    "filter_act$(ProjA2$xs) =filter_act$xs &
     filter_act$(ProjB2$xs) =filter_act$xs"
-apply (tactic {* pair_induct_tac "xs" [] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
 done
 
 
@@ -234,8 +234,8 @@
 lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
    --> Forall (%x. x:act (A||B)) (filter_act$xs)"
 
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
-  thm "sforall_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
+  @{thm sforall_def}] 1 *})
 (* main case *)
 apply auto
 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -255,20 +255,20 @@
   Filter (%a. a:act B)$sch << filter_act$exB
   --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
 
-apply (tactic {* Seq_induct_tac "sch" [thm "Filter_def", thm "Forall_def",
-  thm "sforall_def", thm "mkex_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+  @{thm sforall_def}, @{thm mkex_def}] 1 *})
 
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
 apply auto
 
 (* Case y:A, y:B *)
-apply (tactic {* Seq_case_simp_tac "exA" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
 (* Case exA=UU, Case exA=nil*)
 (* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
    is used! --> to generate a contradiction using  ~a>>ss<< UU(nil), using theorems
    Cons_not_less_UU and Cons_not_less_nil  *)
-apply (tactic {* Seq_case_simp_tac "exB" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
 (* Case exA=a>>x, exB=b>>y *)
 (* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
    as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic
@@ -276,11 +276,11 @@
 apply simp
 
 (* Case y:A, y~:B *)
-apply (tactic {* Seq_case_simp_tac "exA" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
 apply simp
 
 (* Case y~:A, y:B *)
-apply (tactic {* Seq_case_simp_tac "exB" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
 apply simp
 
 (* Case y~:A, y~:B *)
@@ -298,19 +298,21 @@
   val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
 in
 
-fun mkex_induct_tac sch exA exB =
-    EVERY1[Seq_induct_tac sch defs,
-           SIMPSET' asm_full_simp_tac,
+fun mkex_induct_tac ctxt sch exA exB =
+  let val ss = Simplifier.local_simpset_of ctxt in
+    EVERY1[Seq_induct_tac ctxt sch defs,
+           asm_full_simp_tac ss,
            SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
-           Seq_case_simp_tac exA,
-           Seq_case_simp_tac exB,
-           SIMPSET' asm_full_simp_tac,
-           Seq_case_simp_tac exA,
-           SIMPSET' asm_full_simp_tac,
-           Seq_case_simp_tac exB,
-           SIMPSET' asm_full_simp_tac,
-           SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps asigs))
+           Seq_case_simp_tac ctxt exA,
+           Seq_case_simp_tac ctxt exB,
+           asm_full_simp_tac ss,
+           Seq_case_simp_tac ctxt exA,
+           asm_full_simp_tac ss,
+           Seq_case_simp_tac ctxt exB,
+           asm_full_simp_tac ss,
+           asm_full_simp_tac (ss addsimps asigs)
           ]
+  end
 
 end
 *}
@@ -327,7 +329,7 @@
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
 
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
 done
 
 
@@ -356,7 +358,7 @@
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
 done
 
 
@@ -387,7 +389,7 @@
   Filter (%a. a:act B)$sch << filter_act$exB
   --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
       Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
-apply (tactic {* mkex_induct_tac "sch" "exB" "exA" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
 done
 
 (*---------------------------------------------------------------------------
@@ -396,7 +398,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
-apply (tactic {* Seq_induct_tac "y" [] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
 done
 
 
@@ -424,8 +426,8 @@
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
 apply (simp add: ProjA_def Filter_ex_def)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
 apply (rule conjI)
 apply (simp (no_asm) add: mkex_def)
 apply (simplesubst trick_against_eq_in_ass)
@@ -450,7 +452,7 @@
       Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
 
 (* notice necessary change of arguments exA and exB *)
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
 done
 
 
@@ -466,8 +468,8 @@
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
 apply (simp add: ProjB_def Filter_ex_def)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
 apply (rule conjI)
 apply (simp (no_asm) add: mkex_def)
 apply (simplesubst trick_against_eq_in_ass)
@@ -487,7 +489,7 @@
   Filter (%a. a:act B)$sch << filter_act$exB
    --> Forall (%x. fst x : act (A ||B))
          (snd (mkex A B sch (s,exA) (t,exB)))"
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
 done
 
 
@@ -513,7 +515,7 @@
 apply (simp add: compositionality_ex)
 apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
 apply (erule conjE)
 apply (simp add: sch_actions_in_AorB)
 
@@ -524,15 +526,15 @@
 apply (rename_tac exA exB)
 apply (rule_tac x = "mkex A B sch exA exB" in bexI)
 (* mkex actions are just the oracle *)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
 apply (simp add: Mapfst_mkex_is_sch)
 
 (* mkex is an execution -- use compositionality on ex-level *)
 apply (simp add: compositionality_ex)
 apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
 apply (simp add: mkex_actions_in_AorB)
 done
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -199,7 +199,8 @@
   "!!A B. compatible A B ==>  
     ! schA schB. Forall (%x. x:act (A||B)) tr  
     --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (simp add: actions_of_par)
 apply (case_tac "a:act A")
@@ -226,7 +227,8 @@
 lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>  
     ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
     --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
@@ -235,7 +237,8 @@
 lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
     ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
     --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
@@ -411,7 +414,8 @@
   Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
   --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
 
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
 apply auto
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -18,7 +18,7 @@
 apply auto
 apply (frule inp_is_act)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
 apply (rename_tac s ex)
 apply (subgoal_tac "Finite ex")
 prefer 2
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -64,14 +64,14 @@
 apply (rule_tac x = "corresp_ex A f ex" in exI)
 apply auto
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -181,7 +181,7 @@
          !s. reachable C s & is_exec_frag C (s,xs) -->
              mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
 apply (unfold corresp_ex_def)
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* cons case *)
 apply (auto simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
@@ -210,7 +210,7 @@
   --> is_exec_frag A (s,xs @@ ys))"
 
 apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac 1 *})
+apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
 (* main case *)
 apply (auto simp add: split_paired_all)
 done
@@ -230,7 +230,7 @@
 apply (unfold corresp_ex_def)
 
 apply simp
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply auto
 apply (rule_tac t = "f y" in lemma_2_1)
@@ -273,13 +273,13 @@
   apply (rule_tac x = "corresp_ex A f ex" in bexI)
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -324,13 +324,13 @@
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -351,14 +351,14 @@
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -369,5 +369,4 @@
 
 done
 
-
 end
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -1086,44 +1086,46 @@
 done
 
 
-
 ML {*
 
-local
-  val Seq_cases = thm "Seq_cases"
-  val Seq_induct = thm "Seq_induct"
-  val Seq_Finite_ind = thm "Seq_Finite_ind"
-in
-
-fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
-          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+fun Seq_case_tac ctxt s i =
+  RuleInsts.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);
 
 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
-fun Seq_case_simp_tac s i = Seq_case_tac s i THEN SIMPSET' asm_simp_tac (i+2)
-                                             THEN SIMPSET' asm_full_simp_tac (i+1)
-                                             THEN SIMPSET' asm_full_simp_tac i;
+fun Seq_case_simp_tac ctxt s i =
+  let val ss = Simplifier.local_simpset_of ctxt in
+    Seq_case_tac ctxt s i
+    THEN asm_simp_tac ss (i+2)
+    THEN asm_full_simp_tac ss (i+1)
+    THEN asm_full_simp_tac ss i
+  end;
 
 (* rws are definitions to be unfolded for admissibility check *)
-fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
-                         THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac (i+1))))
-                         THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
+fun Seq_induct_tac ctxt s rws i =
+  let val ss = Simplifier.local_simpset_of ctxt in
+    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
+    THEN simp_tac (ss addsimps rws) i
+  end;
 
-fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
-                              THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac i)));
+fun Seq_Finite_induct_tac ctxt i =
+  etac @{thm Seq_Finite_ind} i
+  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
 
-fun pair_tac s = res_inst_tac [("p",s)] PairE
-                          THEN' hyp_subst_tac THEN' SIMPSET' asm_full_simp_tac;
+fun pair_tac ctxt s =
+  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
+  THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
 
 (* induction on a sequence of pairs with pairsplitting and simplification *)
-fun pair_induct_tac s rws i =
-           res_inst_tac [("x",s)] Seq_induct i
-           THEN pair_tac "a" (i+3)
-           THEN (REPEAT_DETERM (CHANGED (SIMPSET' simp_tac (i+1))))
-           THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
-
-end
+fun pair_induct_tac ctxt s rws i =
+  let val ss = Simplifier.local_simpset_of ctxt in
+    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+    THEN pair_tac ctxt "a" (i+3)
+    THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
+    THEN simp_tac (ss addsimps rws) i
+  end;
 
 *}
 
-
 end
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -226,7 +226,7 @@
 apply auto
 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
 apply auto
 apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
 apply (simp (no_asm_simp))
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -172,7 +172,7 @@
          !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
              mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
 
-apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
 (* cons case *)
 apply auto
 apply (rename_tac ex a t s s')
@@ -197,7 +197,7 @@
   !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
   --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
 
-apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply auto
 apply (rename_tac ex a t s s')
@@ -267,7 +267,7 @@
   apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (rename_tac s ex)
   apply (simp (no_asm) add: corresp_ex_sim_def)
   apply (rule_tac s = "s" in traces_coincide_sim)
@@ -275,7 +275,7 @@
   apply (simp add: executions_def reachable.reachable_0 sim_starts1)
 
   (* corresp_ex_sim is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   apply (rename_tac s ex)
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -155,7 +155,7 @@
 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
 apply (unfold tsuffix_def suffix_def)
 apply auto
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply (rule_tac x = "a>>s1" in exI)
 apply auto
 done
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -149,9 +149,9 @@
 
 
 lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic {* pair_tac "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "exec" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 
@@ -170,33 +170,33 @@
 apply (simp split add: split_if)
 (* TL = UU *)
 apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL = nil *)
 apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_tac "y" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_tac @{context} "y" 1 *})
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL =cons *)
 apply (simp add: unlift_def)
 
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply blast
 apply fastsimp
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
  apply fastsimp
 done
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -333,7 +333,7 @@
 declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
 
 lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
-apply (tactic "Seq_Finite_induct_tac 1")
+apply (tactic "Seq_Finite_induct_tac @{context} 1")
 done
 
 
@@ -359,8 +359,8 @@
 lemma execfrag_in_sig: 
   "!! A. is_trans_of A ==>  
   ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
-  thm "Forall_def", thm "sforall_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
+  @{thm Forall_def}, @{thm sforall_def}] 1 *})
 (* main case *)
 apply (auto simp add: is_trans_of_def)
 done
@@ -369,7 +369,7 @@
   "!! A.[|  is_trans_of A; x:executions A |] ==>  
   Forall (%a. a:act A) (filter_act$(snd x))"
 apply (simp add: executions_def)
-apply (tactic {* pair_tac "x" 1 *})
+apply (tactic {* pair_tac @{context} "x" 1 *})
 apply (rule execfrag_in_sig [THEN spec, THEN mp])
 apply auto
 done
@@ -386,10 +386,10 @@
 
 (* only admissible in y, not if done in x !! *)
 lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
-apply (tactic {* pair_induct_tac "y" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
 apply (intro strip)
-apply (tactic {* Seq_case_simp_tac "xa" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 apply auto
 done
 
@@ -401,12 +401,11 @@
 
 lemma exec_prefix2closed [rule_format]:
   "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
-apply (tactic {* pair_induct_tac "x" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
 apply (intro strip)
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 apply auto
 done
 
-
 end
diff -r 548e2d3105b9 -r 5fe899199f85 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -86,17 +86,18 @@
     val prop = Logic.strip_imp_concl t';
     fun tac {prems, context} =
       rewrite_goals_tac defs THEN
-      EVERY (tacs (map (rewrite_rule defs) prems));
+      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
   in Goal.prove_global thy [] asms prop tac end;
 
 fun pg' thy defs t tacsf =
   let
-    fun tacs [] = tacsf
-      | tacs prems = cut_facts_tac prems 1 :: tacsf;
+    fun tacs {prems, context} =
+      if null prems then tacsf context
+      else cut_facts_tac prems 1 :: tacsf context;
   in pg'' thy defs t tacs end;
 
-fun case_UU_tac rews i v =
-  case_split_tac (v^"=UU") i THEN
+fun case_UU_tac ctxt rews i v =
+  InductTacs.case_tac ctxt (v^"=UU") i THEN
   asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac =
@@ -181,7 +182,7 @@
       val appl = bind_fun vars (lhs == rhs);
       val cs = ContProc.cont_thms lam;
       val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
-    in pg (def::betas) appl [rtac reflexive_thm 1] end;
+    in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
 end;
 
 val when_appl = appl_of_def ax_when_def;
@@ -234,7 +235,7 @@
     rewrite_goals_tac [mk_meta_eq iso_swap],
     rtac thm3 1];
 in
-  val exhaust = pg con_appls (mk_trp exh) tacs;
+  val exhaust = pg con_appls (mk_trp exh) (K tacs);
   val casedist =
     standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
 end;
@@ -249,7 +250,7 @@
       val axs = [when_appl, mk_meta_eq rep_strict];
       val goal = bind_fun (mk_trp (strict when_app));
       val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
-    in pg axs goal tacs end;
+    in pg axs goal (K tacs) end;
 
   val when_apps =
     let
@@ -260,7 +261,7 @@
                 mk_trp (when_app`(con_app con args) ===
                        list_ccomb (bound_fun n 0, map %# args))));
           val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
-        in pg axs goal tacs end;
+        in pg axs goal (K tacs) end;
     in mapn one_when 1 cons end;
 end;
 val when_rews = when_strict :: when_apps;
@@ -271,7 +272,7 @@
   fun dis_strict (con, _) =
     let
       val goal = mk_trp (strict (%%:(dis_name con)));
-    in pg axs_dis_def goal [rtac when_strict 1] end;
+    in pg axs_dis_def goal (K [rtac when_strict 1]) end;
 
   fun dis_app c (con, args) =
     let
@@ -279,7 +280,7 @@
       val rhs = if con = c then TT else FF;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_dis_def goal tacs end;
+    in pg axs_dis_def goal (K tacs) end;
 
   val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
 
@@ -291,7 +292,7 @@
          contr_tac 1,
          DETERM_UNTIL_SOLVED (CHANGED
           (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
-    in pg [] goal tacs end;
+    in pg [] goal (K tacs) end;
 
   val dis_stricts = map dis_strict cons;
   val dis_defins = map dis_defin cons;
@@ -304,7 +305,7 @@
     let
       val goal = mk_trp (strict (%%:(mat_name con)));
       val tacs = [rtac when_strict 1];
-    in pg axs_mat_def goal tacs end;
+    in pg axs_mat_def goal (K tacs) end;
 
   val mat_stricts = map mat_strict cons;
 
@@ -317,7 +318,7 @@
         else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_mat_def goal tacs end;
+    in pg axs_mat_def goal (K tacs) end;
 
   val mat_apps =
     maps (fn (c,_) => map (one_mat c) cons) cons;
@@ -340,7 +341,7 @@
       val axs = @{thm branch_def} :: axs_pat_def;
       val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
       val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
-    in pg axs goal tacs end;
+    in pg axs goal (K tacs) end;
 
   fun pat_app c (con, args) =
     let
@@ -349,7 +350,7 @@
       val rhs = if con = fst c then pat_rhs c else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs goal tacs end;
+    in pg axs goal (K tacs) end;
 
   val pat_stricts = map pat_strict cons;
   val pat_apps = maps (fn c => map (pat_app c) cons) cons;
@@ -366,16 +367,16 @@
           fun f arg = if vname arg = vn then UU else %# arg;
           val goal = mk_trp (con_app2 con f args === UU);
           val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
-        in pg con_appls goal tacs end;
+        in pg con_appls goal (K tacs) end;
     in map one_strict (nonlazy args) end;
 
   fun con_defin (con, args) =
     let
       val concl = mk_trp (defined (con_app con args));
       val goal = lift_defined %: (nonlazy args, concl);
-      val tacs = [
+      fun tacs ctxt = [
         rtac @{thm rev_contrapos} 1,
-        eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
+        RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
         asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
     in pg [] goal tacs end;
 in
@@ -394,7 +395,7 @@
       val tacs = [
         rtac (iso_locale RS iso_compact_abs) 1,
         REPEAT (resolve_tac rules 1 ORELSE atac 1)];
-    in pg con_appls goal tacs end;
+    in pg con_appls goal (K tacs) end;
 in
   val con_compacts = map con_compact cons;
 end;
@@ -402,7 +403,7 @@
 local
   fun one_sel sel =
     pg axs_sel_def (mk_trp (strict (%%:sel)))
-      [simp_tac (HOLCF_ss addsimps when_rews) 1];
+      (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
 
   fun sel_strict (_, args) =
     List.mapPartial (Option.map one_sel o sel_of) args;
@@ -419,20 +420,20 @@
       val nlas' = List.filter (fn v => v <> vnn) nlas;
       val lhs = (%%:sel)`(con_app con args);
       val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
-      val tacs1 =
+      fun tacs1 ctxt =
         if vnn mem nlas
-        then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
+        then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
         else [];
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_sel_def goal (tacs1 @ tacs2) end;
+    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 
   fun sel_app_diff c n sel (con, args) =
     let
       val nlas = nonlazy args;
       val goal = mk_trp (%%:sel ` con_app con args === UU);
-      val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
+      fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
-    in pg axs_sel_def goal (tacs1 @ tacs2) end;
+    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 
   fun sel_app c n sel (con, args) =
     if con = c
@@ -456,7 +457,7 @@
         contr_tac 1,
         DETERM_UNTIL_SOLVED (CHANGED
           (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
-    in pg [] goal tacs end;
+    in pg [] goal (K tacs) end;
 in
   val sel_defins =
     if length cons = 1
@@ -474,10 +475,10 @@
       let
         val goal = lift_defined %: (nonlazy args1,
                         mk_trp (con_app con1 args1 ~<< con_app con2 args2));
-        val tacs = [
+        fun tacs ctxt = [
           rtac @{thm rev_contrapos} 1,
-          eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
-          @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
+          RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
+          @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
           @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
       in pg [] goal tacs end;
 
@@ -527,13 +528,13 @@
       val abs_less = ax_abs_iso RS (allI RS injection_less);
       val tacs =
         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
-    in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
+    in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
 
   val injects =
     let
       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
       val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
-    in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
+    in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
 end;
 
 (* ----- theorems concerning one induction step ----------------------------- *)
@@ -542,7 +543,7 @@
   let
     val goal = mk_trp (strict (dc_copy `% "f"));
     val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
-  in pg [ax_copy_def] goal tacs end;
+  in pg [ax_copy_def] goal (K tacs) end;
 
 local
   fun copy_app (con, args) =
@@ -552,9 +553,9 @@
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
       val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
       val stricts = abs_strict::when_strict::con_stricts;
-      val tacs1 = map (case_UU_tac stricts 1 o vname) args';
+      fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
-    in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
+    in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 in
   val copy_apps = map copy_app cons;
 end;
@@ -564,7 +565,7 @@
     let
       val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
       val rews = copy_strict :: copy_apps @ con_rews;
-      val tacs = map (case_UU_tac rews 1) (nonlazy args) @
+      fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
         [asm_simp_tac (HOLCF_ss addsimps rews) 1];
     in pg [] goal tacs end;
 
@@ -646,8 +647,8 @@
     let
       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
       val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
-      val tacs = [
-        nat_induct_tac "n" 1,
+      fun tacs ctxt = [
+        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
         simp_tac iterate_Cprod_ss 1,
         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
     in pg copy_take_defs goal tacs end;
@@ -656,9 +657,9 @@
   fun take_0 n dn =
     let
       val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
-    in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
+    in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
-  val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
+  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
   val take_apps =
     let
       fun mk_eqn dn (con, args) =
@@ -670,19 +671,19 @@
       fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
       val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
       val simps = List.filter (has_fewer_prems 1) copy_rews;
-      fun con_tac (con, args) =
+      fun con_tac ctxt (con, args) =
         if nonlazy_rec args = []
         then all_tac
-        else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
+        else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
           asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
-      fun eq_tacs ((dn, _), cons) = map con_tac cons;
-      val tacs =
+      fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
+      fun tacs ctxt =
         simp_tac iterate_Cprod_ss 1 ::
-        nat_induct_tac "n" 1 ::
+        InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
         simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
         TRY (safe_tac HOL_cs) ::
-        maps eq_tacs eqs;
+        maps (eq_tacs ctxt) eqs;
     in pg copy_take_defs goal tacs end;
 in
   val take_rews = map standard
@@ -705,8 +706,8 @@
     (mapn (fn n => fn x => (P_name n, x)) 1 conss,
      mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
   val take_ss = HOL_ss addsimps take_rews;
-  fun quant_tac i = EVERY
-    (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
+  fun quant_tac ctxt i = EVERY
+    (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
 
   fun ind_prems_tac prems = EVERY
     (maps (fn cons =>
@@ -745,16 +746,16 @@
       fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
       val goal = ind_term concf;
 
-      fun tacf prems =
+      fun tacf {prems, context} =
         let
           val tacs1 = [
-            quant_tac 1,
+            quant_tac context 1,
             simp_tac HOL_ss 1,
-            nat_induct_tac "n" 1,
+            InductTacs.induct_tac context [[SOME "n"]] 1,
             simp_tac (take_ss addsimps prems) 1,
             TRY (safe_tac HOL_cs)];
           fun arg_tac arg =
-            case_UU_tac (prems @ con_rews) 1
+            case_UU_tac context (prems @ con_rews) 1
               (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
           fun con_tacs (con, args) = 
             asm_simp_tac take_ss 1 ::
@@ -763,7 +764,7 @@
             map (K (atac 1))      (nonlazy args) @
             map (K (etac spec 1)) (List.filter is_rec args);
           fun cases_tacs (cons, cases) =
-            res_inst_tac [("x","x")] cases 1 ::
+            RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
             asm_simp_tac (take_ss addsimps prems) 1 ::
             maps con_tacs cons;
         in
@@ -779,9 +780,9 @@
           val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
           val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
           val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
-          fun tacf prems = [
-            res_inst_tac [("t", x_name n    )] (ax_reach RS subst) 1,
-            res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
+          fun tacf {prems, context} = [
+            RuleInsts.res_inst_tac context [(("t", 0), x_name n    )] (ax_reach RS subst) 1,
+            RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
             stac fix_def2 1,
             REPEAT (CHANGED
               (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
@@ -814,7 +815,7 @@
               resolve_tac take_lemmas 1,
               asm_simp_tac take_ss 1,
               atac 1];
-          in pg [] goal tacs end;
+          in pg [] goal (K tacs) end;
         val finite_lemmas1a = map dname_lemma dnames;
  
         val finite_lemma1b =
@@ -829,33 +830,33 @@
               end;
             val goal =
               mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
-            fun arg_tacs vn = [
-              eres_inst_tac [("x", vn)] all_dupE 1,
+            fun arg_tacs ctxt vn = [
+              RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
               etac disjE 1,
               asm_simp_tac (HOL_ss addsimps con_rews) 1,
               asm_simp_tac take_ss 1];
-            fun con_tacs (con, args) =
+            fun con_tacs ctxt (con, args) =
               asm_simp_tac take_ss 1 ::
-              maps arg_tacs (nonlazy_rec args);
-            fun foo_tacs n (cons, cases) =
+              maps (arg_tacs ctxt) (nonlazy_rec args);
+            fun foo_tacs ctxt n (cons, cases) =
               simp_tac take_ss 1 ::
               rtac allI 1 ::
-              res_inst_tac [("x",x_name n)] cases 1 ::
+              RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
               asm_simp_tac take_ss 1 ::
-              maps con_tacs cons;
-            val tacs =
+              maps (con_tacs ctxt) cons;
+            fun tacs ctxt =
               rtac allI 1 ::
-              nat_induct_tac "n" 1 ::
+              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
               simp_tac take_ss 1 ::
               TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
-              flat (mapn foo_tacs 1 (conss ~~ cases));
+              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
           in pg [] goal tacs end;
 
         fun one_finite (dn, l1b) =
           let
             val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
-            val tacs = [
-              case_UU_tac take_rews 1 "x",
+            fun tacs ctxt = [
+              case_UU_tac ctxt take_rews 1 "x",
               eresolve_tac finite_lemmas1a 1,
               step_tac HOL_cs 1,
               step_tac HOL_cs 1,
@@ -867,7 +868,7 @@
         val ind =
           let
             fun concf n dn = %:(P_name n) $ %:(x_name n);
-            fun tacf prems =
+            fun tacf {prems, context} =
               let
                 fun finite_tacs (finite, fin_ind) = [
                   rtac(rewrite_rule axs_finite_def finite RS exE)1,
@@ -893,9 +894,9 @@
             fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
             fun concf n dn = %:(P_name n) $ %:(x_name n);
           in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
-        fun tacf prems =
+        fun tacf {prems, context} =
           map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
-          quant_tac 1,
+          quant_tac context 1,
           rtac (adm_impl_admw RS wfix_ind) 1,
           REPEAT_DETERM (rtac adm_all 1),
           REPEAT_DETERM (
@@ -930,18 +931,18 @@
           Library.foldr mk_all2 (xs,
             Library.foldr mk_imp (mapn mk_prj 0 dnames,
               foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
-      fun x_tacs n x = [
+      fun x_tacs ctxt n x = [
         rotate_tac (n+1) 1,
         etac all2E 1,
-        eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+        RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
         TRY (safe_tac HOL_cs),
         REPEAT (CHANGED (asm_simp_tac take_ss 1))];
-      val tacs = [
+      fun tacs ctxt = [
         rtac impI 1,
-        nat_induct_tac "n" 1,
+        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
         simp_tac take_ss 1,
         safe_tac HOL_cs] @
-        flat (mapn x_tacs 0 xs);
+        flat (mapn (x_tacs ctxt) 0 xs);
     in pg [ax_bisim_def] goal tacs end;
 in
   val coind = 
@@ -959,7 +960,7 @@
           cut_facts_tac [coind_lemma] 1,
           fast_tac HOL_cs 1])
         take_lemmas;
-    in pg [] goal tacs end;
+    in pg [] goal (K tacs) end;
 end; (* local *)
 
 in thy |> Sign.add_path comp_dnam
diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/LCF.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -23,7 +23,7 @@
 typedecl ('a,'b) "+"    (infixl 5)
 
 arities
-  fun :: (cpo, cpo) cpo
+  "fun" :: (cpo, cpo) cpo
   "*" :: (cpo, cpo) cpo
   "+" :: (cpo, cpo) cpo
   tr :: cpo
@@ -316,13 +316,13 @@
 
 
 ML {*
-  fun induct_tac v i =
-    res_inst_tac[("f",v)] @{thm induct} i THEN
+  fun induct_tac ctxt v i =
+    RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
     REPEAT (resolve_tac @{thms adm_lemmas} i)
 *}
 
 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
-  apply (tactic {* induct_tac "f" 1 *})
+  apply (tactic {* induct_tac @{context} "f" 1 *})
   apply (rule minimal)
   apply (intro strip)
   apply (erule subst)
@@ -375,8 +375,8 @@
   done
 
 ML {*
-fun induct2_tac (f,g) i =
-  res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
+fun induct2_tac ctxt (f, g) i =
+  RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
   REPEAT(resolve_tac @{thms adm_lemmas} i)
 *}
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/ex/Ex1.thy
--- a/src/LCF/ex/Ex1.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex1.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -32,7 +32,7 @@
   done
 
 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
-  apply (tactic {* induct_tac "K" 1 *})
+  apply (tactic {* induct_tac @{context} "K" 1 *})
   apply (simp (no_asm))
   apply (simp (no_asm) split: COND_cases_iff)
   apply (intro strip)
diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/ex/Ex2.thy
--- a/src/LCF/ex/Ex2.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex2.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -23,7 +23,7 @@
 
 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
   apply (simplesubst H)
-  apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+  apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
   apply (simp (no_asm))
   apply (simp (no_asm_simp) split: COND_cases_iff)
   done
diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex3.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -18,7 +18,7 @@
 declare p_strict [simp] p_s [simp]
 
 lemma example: "p(FIX(s),y) = FIX(s)"
-  apply (tactic {* induct_tac "s" 1 *})
+  apply (tactic {* induct_tac @{context} "s" 1 *})
   apply (simp (no_asm))
   apply (simp (no_asm))
   done
diff -r 548e2d3105b9 -r 5fe899199f85 src/LCF/ex/Ex4.thy
--- a/src/LCF/ex/Ex4.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex4.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -10,7 +10,7 @@
   shows "FIX(f)=p"
   apply (unfold eq_def)
   apply (rule conjI)
-  apply (tactic {* induct_tac "f" 1 *})
+  apply (tactic {* induct_tac @{context} "f" 1 *})
   apply (rule minimal)
   apply (intro strip)
   apply (rule less_trans)
diff -r 548e2d3105b9 -r 5fe899199f85 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/Sequents/LK0.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -156,12 +156,12 @@
 
 ML {*
 (*Cut and thin, replacing the right-side formula*)
-fun cutR_tac s i =
-  res_inst_tac [ ("P", s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
+fun cutR_tac ctxt s i =
+  RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
 
 (*Cut and thin, replacing the left-side formula*)
-fun cutL_tac s i =
-  res_inst_tac [("P", s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
+fun cutL_tac ctxt s i =
+  RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
 *}
 
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -10,8 +10,8 @@
 
 signature DATATYPE_TACTICS =
 sig
-  val induct_tac: string -> int -> tactic
-  val exhaust_tac: string -> int -> tactic
+  val induct_tac: Proof.context -> string -> int -> tactic
+  val exhaust_tac: Proof.context -> string -> int -> tactic
   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
   val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
     (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
@@ -89,10 +89,10 @@
       (2) exhaustion works for VARIABLES in the premises, not general terms
 **)
 
-fun exhaust_induct_tac exh var i state =
+fun exhaust_induct_tac exh ctxt var i state =
   let
+    val thy = ProofContext.theory_of ctxt
     val (_, _, Bi, _) = dest_state (state, i)
-    val thy = Thm.theory_of_thm state
     val tn = find_tname var Bi
     val rule =
         if exh then #exhaustion (datatype_info thy tn)
@@ -102,11 +102,11 @@
              [] => error "induction is not available for this datatype"
            | major::_ => FOLogic.dest_Trueprop major)
   in
-    Tactic.eres_inst_tac' [(ixn, var)] rule i state
+    RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
   end
   handle Find_tname msg =>
             if exh then (*try boolean case analysis instead*)
-                case_tac var i state
+                case_tac ctxt var i state
             else error msg;
 
 val exhaust_tac = exhaust_induct_tac true;
@@ -178,9 +178,9 @@
 
 val setup =
   Method.add_methods
-    [("induct_tac", Method.goal_args Args.name induct_tac,
+    [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
       "induct_tac emulation (dynamic instantiation!)"),
-     ("case_tac", Method.goal_args Args.name exhaust_tac,
+     ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
       "datatype case_tac emulation (dynamic instantiation!)")];
 
 
diff -r 548e2d3105b9 -r 5fe899199f85 src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/ZF/UNITY/SubstAx.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -360,7 +360,7 @@
                                     @{thm EnsuresI}, @{thm ensuresI}] 1),
               (*now there are two subgoals: co & transient*)
               simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
-              res_inst_tac [("act", sact)] @{thm transientI} 2,
+              RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [@{thm domain_def}]) 3, 
               (* proving the domain part *)