diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/J/Term.thy
+(*  Title:      HOL/MicroJava/J/Value.thy
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
@@ -6,12 +6,12 @@
 Java values
 *)
 
-Value = Type +
+theory Value = Type:
 
-types   loc     (* locations, i.e. abstract references on objects *)
-arities loc :: term
+typedecl loc (* locations, i.e. abstract references on objects *)
+arities loc :: "term"
 
-datatype val_   (* name non 'val' because of clash with ML token *)
+datatype val
   = Unit        (* dummy result value of void methods *)
   | Null        (* null reference *)
   | Bool bool   (* Boolean value *)
@@ -19,9 +19,6 @@
                    of clash with HOL/Set.thy *)
   | Addr loc    (* addresses, i.e. locations of objects *)
 
-types	val = val_
-translations "val" <= (type) "val_"
-
 consts
   the_Bool :: "val => bool"
   the_Intg :: "val => int"