
diff -r 59c117a0bcf3 -r a47e4fd7ebc1 src/HOL/MicroJava/J/WellForm.thy
--- 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)




