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