diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/ex/Antiquote.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -13,10 +13,10 @@
 *}
 
 syntax
-  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
+  "_Expr" :: "'a => 'a"                         ("EXPR _" [1000] 999)
 
 constdefs
-  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
+  var :: "'a => ('a => nat) => nat"             ("VAR _" [1000] 999)
   "var x env == env x"
 
   Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
@@ -29,9 +29,9 @@
 term "EXPR (a + b + c + VAR x + VAR y + 1)"
 term "EXPR (VAR (f w) + VAR x)"
 
-term "Expr (\<lambda>env. env x)"				(*improper*)
+term "Expr (\<lambda>env. env x)"    -- {* improper *}
 term "Expr (\<lambda>env. f env)"
-term "Expr (\<lambda>env. f env + env x)"			(*improper*)
+term "Expr (\<lambda>env. f env + env x)"    -- {* improper *}
 term "Expr (\<lambda>env. f env y z)"
 term "Expr (\<lambda>env. f env + g y env)"
 term "Expr (\<lambda>env. f env + g env y + h a env z)"