# HG changeset patch
# User wenzelm
# Date 1006445528 -3600
# Node ID 9c356e2da72fa5417d810ea1a921b6cb6a8b1532
# Parent  6f2acf10e2a27b5760316a03211a1eba16462f0b
renamed "fields" to "flds" (avoid clash with new "fields" operation);

diff -r 6f2acf10e2a2 -r 9c356e2da72f src/HOL/NanoJava/Decl.thy
--- 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 *}
diff -r 6f2acf10e2a2 -r 9c356e2da72f src/HOL/NanoJava/TypeRel.thy
--- 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