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