--- a/src/HOL/MicroJava/J/Value.thy Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Sun Sep 30 21:55:15 2007 +0200
@@ -8,11 +8,11 @@
theory Value imports Type begin
-typedecl loc_ -- "locations, i.e. abstract references on objects"
+typedecl loc' -- "locations, i.e. abstract references on objects"
datatype loc
= XcptRef xcpt -- "special locations for pre-allocated system exceptions"
- | Loc loc_ -- "usual locations (references on objects)"
+ | Loc loc' -- "usual locations (references on objects)"
datatype val
= Unit -- "dummy result value of void methods"