--- a/src/HOL/NanoJava/TypeRel.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Sat Nov 01 14:20:38 2014 +0100
@@ -114,7 +114,7 @@
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
apply (unfold method_def)
-apply (erule (1) class_rec [THEN trans]);
+apply (erule (1) class_rec [THEN trans])
apply simp
done
@@ -126,7 +126,7 @@
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
apply (unfold field_def)
-apply (erule (1) class_rec [THEN trans]);
+apply (erule (1) class_rec [THEN trans])
apply simp
done