--- a/src/HOL/NanoJava/State.thy Thu Aug 09 22:07:39 2001 +0200
+++ b/src/HOL/NanoJava/State.thy Thu Aug 09 23:42:45 2001 +0200
@@ -15,7 +15,6 @@
text {* locations, i.e.\ abstract references to objects *}
typedecl loc
-arities loc :: "term"
datatype val
= Null (* null reference *)
--- a/src/HOL/NanoJava/Term.thy Thu Aug 09 22:07:39 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Thu Aug 09 23:42:45 2001 +0200
@@ -11,9 +11,6 @@
typedecl cname (* class name *)
typedecl vnam (* variable or field name *)
typedecl mname (* method name *)
-arities cname :: "term"
- vnam :: "term"
- mname :: "term"
types imname = "cname \<times> mname"
datatype vname (* variable for special names *)