--- a/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 22:13:39 2008 +0200
@@ -108,8 +108,8 @@
apply (rule hoare_ehoare.induct)
(*18*)
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 (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast