--- a/src/HOL/NanoJava/Equivalence.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Mar 25 10:44:57 2015 +0100
@@ -105,8 +105,8 @@
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y" []) *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y" []) *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare _ _" []) *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare _ _" []) *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast