diff -r 46db6fde4ee3 -r c7226e6f9625 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Mon Sep 25 12:04:10 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Mon Sep 25 12:08:49 2000 +0200
@@ -8,23 +8,23 @@
 
 Term = Value + 
 
-datatype binop = Eq | Add	   (* function codes for binary operation *)
+datatype binop = Eq | Add    (* function codes for binary operation *)
 
 datatype expr
-	= NewC	cname              (* class instance creation *)
-	| Cast	cname expr         (* type cast *)
-	| Lit	val                  (* literal value, also references *)
-  | BinOp binop  expr expr   (* binary operation *)
-	| LAcc vname               (* local (incl. parameter) access *)
-	| LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
-	| FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
-	| FAss cname expr vname 
+  = NewC cname               (* class instance creation *)
+  | Cast cname expr          (* type cast *)
+  | Lit val                  (* literal value, also references *)
+  | BinOp binop expr expr    (* binary operation *)
+  | LAcc vname               (* local (incl. parameter) access *)
+  | LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
+  | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
+  | FAss cname expr vname 
                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
-	| Call expr mname 
+  | Call expr mname 
     (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
 
 and stmt
-	= Skip                     (* empty statement *)
+  = Skip                     (* empty statement *)
   | Expr expr                (* expression statement *)
   | Comp stmt stmt       ("_;; _"             [61,60]60)
   | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)