diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 25 10:44:57 2015 +0100
@@ -419,7 +419,7 @@
 apply( simp)
 apply( drule map_add_SomeD)
 apply( erule disjE)
-apply(  erule_tac V = "?P --> ?Q" in thin_rl)
+apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: wf_cdecl_def)
 apply( clarify)
@@ -454,7 +454,7 @@
 apply( simp)
 apply( drule map_add_SomeD)
 apply( erule disjE)
-apply(  erule_tac V = "?P --> ?Q" in thin_rl)
+apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: ws_cdecl_def)
 apply blast
@@ -486,7 +486,7 @@
 apply(  assumption)
 apply( unfold map_add_def)
 apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
-apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
+apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, C, m)) ms) sig = Some z" for C)
 apply(  erule exE)
 apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
 prefer 2