diff -r 3242637f668c -r ac86b3d44730 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon May 15 17:32:39 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Mon May 15 17:34:05 2000 +0200
@@ -8,23 +8,24 @@
 
 State = WellType +
 
-constdefs
-
+consts
   the_Bool	:: "val \\<Rightarrow> bool"
- "the_Bool v  \\<equiv> \\<epsilon>b. v = Bool b"
-
   the_Int	:: "val \\<Rightarrow> int"
- "the_Int  v  \\<equiv> \\<epsilon>i. v = Intg i"
-
   the_Addr	:: "val \\<Rightarrow> loc"
- "the_Addr  v  \\<equiv> \\<epsilon>a. v = Addr a"
-
-consts
 
   defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
   default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
 
 primrec
+ "the_Bool (Bool b) = b"
+
+primrec
+ "the_Int (Intg i) = i"
+
+primrec
+ "the_Addr (Addr a) = a"
+
+primrec
 	"defpval Void    = Unit"
 	"defpval Boolean = Bool False"
 	"defpval Integer = Intg (#0)"