diff -r 0bd9eedaa301 -r 51f3d31e8eea src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Nov 22 11:53:56 2004 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Nov 22 11:54:08 2004 +0100
@@ -371,8 +371,6 @@
   {((Class Base, Class Base), [Class Base])}"
 apply (unfold appl_methds_def)
 apply (simp (no_asm))
-apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
-apply  (auto simp add: map_of_Cons foo_Base_def)
 done
 
 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =