diff -r b31c2132176a -r f4d76cb26433 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Tue Jul 04 01:12:42 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Tue Jul 04 10:54:32 2000 +0200
@@ -10,7 +10,7 @@
 
 consts
   the_Bool	:: "val \\<Rightarrow> bool"
-  the_Int	:: "val \\<Rightarrow> int"
+  the_Intg	:: "val \\<Rightarrow> int"
   the_Addr	:: "val \\<Rightarrow> loc"
 
   defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
@@ -20,7 +20,7 @@
  "the_Bool (Bool b) = b"
 
 primrec
- "the_Int (Intg i) = i"
+ "the_Intg (Intg i) = i"
 
 primrec
  "the_Addr (Addr a) = a"