diff -r 4522e59b7d84 -r fe82134773dc src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:53 2000 +0200
@@ -14,7 +14,6 @@
         obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
 
 constdefs
-
   obj_ty	:: "obj => ty"
  "obj_ty obj  == Class (fst obj)"
 
@@ -42,9 +41,9 @@
   Norm		:: "state => xstate"
 
 translations
-  "heap"	=> "fst"
-  "locals"	=> "snd"
-  "Norm s"      == "(None,s)"  
+  "heap"   => "fst"
+  "locals" => "snd"
+  "Norm s" == "(None,s)"  
 
 constdefs