src/HOL/MicroJava/J/Value.thy
changeset 24783 5a3e336a2e37
parent 16417 9bc16273c2d4
child 39758 b8a53e3a0ee2
--- 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"