--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Mar 25 10:44:57 2015 +0100
@@ -137,20 +137,20 @@
apply( clarsimp)
apply( drule (3) Call_lemma)
apply( clarsimp simp add: wf_java_mdecl_def)
-apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
+apply( erule_tac V = "method sig x = y" for sig x y in thin_rl)
apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
apply( rule conformsI)
apply( erule conforms_heapD)
apply( rule lconf_ext)
apply( force elim!: Call_lemma2)
apply( erule conf_hext, erule (1) conf_obj_AddrI)
-apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply( erule_tac V = "E\<turnstile>blk\<surd>" for E blk in thin_rl)
apply (simp add: conforms_def)
apply( erule conjE)
apply( drule spec, erule (1) impE)
apply( drule spec, erule (1) impE)
-apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
+apply( erule_tac V = "E\<turnstile>res::rT" for E rT in thin_rl)
apply( clarify)
apply( rule conjI)
apply( fast intro: hext_trans)
@@ -291,7 +291,7 @@
-- "5 While"
prefer 5
-apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
+apply(erule_tac V = "a \<longrightarrow> b" for a b in thin_rl)
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
apply(force elim: hext_trans)