--- a/src/HOL/NanoJava/Decl.thy Wed Nov 21 20:20:18 2001 +0100
+++ b/src/HOL/NanoJava/Decl.thy Thu Nov 22 17:12:08 2001 +0100
@@ -28,7 +28,7 @@
record class
= super :: cname
- fields ::"fdecl list"
+ flds ::"fdecl list"
methods ::"mdecl list"
text{* Class declaration *}
--- a/src/HOL/NanoJava/TypeRel.thy Wed Nov 21 20:20:18 2001 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Nov 22 17:12:08 2001 +0100
@@ -133,10 +133,10 @@
--{* Fields of a class, with inheritance and hiding *}
-defs field_def: "field C \<equiv> class_rec C fields"
+defs field_def: "field C \<equiv> class_rec C flds"
-lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
-field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
+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 simp