# HG changeset patch
# User wenzelm
# Date 997393365 -7200
# Node ID 7a7bb59a05dbe28ede8a36d7bc28202ba2df8e15
# Parent  681aa3dfab4b0ea98415fdd2faf49cb15ae7a533
removed obsolete "arities";

diff -r 681aa3dfab4b -r 7a7bb59a05db src/HOL/NanoJava/State.thy
--- 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 *)
diff -r 681aa3dfab4b -r 7a7bb59a05db src/HOL/NanoJava/Term.thy
--- 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 *)