--- a/src/HOL/MicroJava/J/Example.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Sun Nov 20 21:05:23 2011 +0100
@@ -202,7 +202,7 @@
apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
done
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
apply (rule subcls_direct)