--- a/src/HOL/MicroJava/J/WellForm.thy Wed Apr 11 08:28:13 2007 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Apr 11 08:28:14 2007 +0200
@@ -505,7 +505,7 @@
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
prefer 2
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
-apply( tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
+apply( tactic "asm_full_simp_tac (HOL_ss addsimps [@{thm not_None_eq} RS sym]) 1")
apply( simp_all (no_asm_simp) del: split_paired_Ex)
apply( frule (1) class_wf)
apply( simp (no_asm_simp) only: split_tupled_all)