diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -322,7 +322,7 @@
     apply (frule is_type_pTs [OF wf], assumption+)
     apply clarify
     apply (drule rule [OF wf], assumption+)
-    apply (rule refl)
+    apply (rule HOL.refl)
     apply assumption+
     done
 qed