--- 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)