src/HOL/MicroJava/J/Type.thy
changeset 12338 de0f4a63baa5
parent 11070 cc421547e744
child 12517 360e3215f029
--- a/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -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"
 
 datatype vname    (* names for This pointer and local/field variables *)
   = This