diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/NanoJava/Equivalence.thy
--- 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