src/HOL/MicroJava/J/Type.thy
changeset 12338 de0f4a63baa5
parent 11070 cc421547e744
child 12517 360e3215f029
     1.1 --- a/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -11,9 +11,6 @@
     1.4  typedecl cname  (* class name *)
     1.5  typedecl vnam   (* variable or field name *)
     1.6  typedecl mname  (* method name *)
     1.7 -arities  cname :: "term"
     1.8 -         vnam  :: "term"
     1.9 -         mname :: "term"
    1.10  
    1.11  datatype vname    (* names for This pointer and local/field variables *)
    1.12    = This