diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed May 02 01:42:23 2007 +0200
@@ -14,15 +14,17 @@
 
 atom_decl name 
 
-nominal_datatype ty = TBase 
-                    | TUnit 
-                    | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty = 
+    TBase 
+  | TUnit 
+  | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trm = Unit
-                     | Var "name"
-                     | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
-                     | App "trm" "trm"
-                     | Const "nat"
+nominal_datatype trm = 
+    Unit
+  | Var "name"
+  | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+  | App "trm" "trm"
+  | Const "nat"
 
 types Ctxt  = "(name\<times>ty) list"
 types Subst = "(name\<times>trm) list"