diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/MicroJava/J/Example.thy
--- 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)