diff -r e2c0138b5cea -r 13d7ea419c5f ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -1109,9 +1109,9 @@
 *}
 
 ML %grayML{*
-structure Result = 
-  Proof_Data (type T = unit -> term
-              fun init thy () = error "Result")
+structure Result = Proof_Data 
+  (type T = unit -> term
+   fun init thy () = error "Result")
 
 val result_cookie = (Result.get, Result.put, "Result.put") *}