diff -r 034150db9d91 -r c3dbc04471a9 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Wed May 22 13:24:30 2019 +0200
@@ -663,7 +663,8 @@
 \<close>
 
 ML %grayML\<open>fun filtered_input' str = 
-       filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str)\<close>
+  filter Token.is_proper 
+    (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str)\<close>
 
 text \<open>
   where we pretend the parsed string starts on line 7. An example is
@@ -770,7 +771,8 @@
 
 @{ML_response [display,gray]
 \<open>let 
-  val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) "foo"
+  val input = Token.explode (Thy_Header.get_keywords' @{context}) 
+    (Position.line 42) "foo"
 in 
   YXML.parse (fst (Parse.term input))
 end\<close>
@@ -1140,7 +1142,7 @@
 end\<close>
 
 text \<open>
-  In Line 12, we implement a parser that first reads in an optional lemma name (terminated 
+  In Line 13, we implement a parser that first reads in an optional lemma name (terminated 
   by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
   and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
   in the structure @{ML_structure Code_Runtime}.  Once the ML-text has been turned into a term,