--- a/ProgTutorial/First_Steps.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Wed May 22 13:24:30 2019 +0200
@@ -880,9 +880,9 @@
 setup %gray \<open>term_pat_setup\<close>
 
 text \<open>
-  The parser in Line 2 provides us with a context and a string; this string is
+  The parser in Line 3 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
-  Proof_Context} (Line 5); the next two lines transform the term into a string
+  Proof_Context} (Line 6); the next two lines transform the term into a string
   so that the ML-system can understand it. (All these functions will be explained
   in more detail in later sections.) An example for this antiquotation is:
 

--- a/ProgTutorial/Package/Ind_Code.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed May 22 13:24:30 2019 +0200
@@ -142,14 +142,12 @@
 
 text \<open>
   The user will state the introduction rules using meta-implications and
-  meta-quanti\-fications. In Line 4, we transform these introduction rules
+  meta-quanti\-fications. In Line 3, we transform these introduction rules
   into the object logic (since definitions cannot be stated with
-  meta-connectives). To do this transformation we have to obtain the theory
-  behind the local theory using the function @{ML_ind theory_of in Proof_Context} 
-  (Line 3); with this theory we can use the function
-  @{ML_ind  atomize_term in Object_Logic} to make the transformation (Line 4). The call
-  to @{ML defn_aux} in Line 5 produces all right-hand sides of the
-  definitions. The actual definitions are then made in Line 7.  The result of
+  meta-connectives). We use the function
+  @{ML_ind atomize_term in Object_Logic} to make the transformation (Line 3). The call
+  to @{ML defn_aux} in Line 4 produces all right-hand sides of the
+  definitions. The actual definitions are then made in Line 6.  The result of
   the function is a list of theorems and a local theory (the theorems are
   registered with the local theory). A testcase for this function is
 \<close>
@@ -848,7 +846,7 @@
   connective is \<open>\<forall>\<close>.
   
   The function @{ML prove_intro_tac} only needs to be changed so that it
-  gives the context to @{ML prepare_prem} (Line 8). The modified version
+  gives the context to @{ML prepare_prem} (Line 10). The modified version
   is below.
 \<close>
 

--- 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, 

--- a/ProgTutorial/Recipes/Antiquotes.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Wed May 22 13:24:30 2019 +0200
@@ -34,7 +34,7 @@
   @{text [display] \<open>@{ML_checked "a_piece_of_code"}\<close>}
 
   The code is checked by sending the ML-expression @{text [quotes] "val _ =
-  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_source_in\<close>} in Line 7 below). The complete code of the
+  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_in\<close>} in Line 8 below). The complete code of the
   document antiquotation is as follows:
 
 \<close>
@@ -59,40 +59,25 @@
 
 
 text \<open>
-  The parser @{ML \<open>(Scan.lift Args.name)\<close>} in Line 7 parses a string, in this
-  case the code, and then calls the function @{ML output_ml}. As mentioned
-  before, the parsed code is sent to the ML-compiler in Line 4 using the
+  The parser @{ML \<open>(Scan.lift Args.text_input)\<close>} in Line 15 parses a string, in this
+  case the code, and then we call the function @{ML output_ml}. As mentioned
+  before, the parsed code is sent to the ML-compiler in Line 8 using the
   function @{ML ml_val}, which constructs the appropriate ML-expression, and
   using @{ML \<open>eval_in\<close> in ML_Context}, which calls the compiler.  If the code is
-  ``approved'' by the compiler, then the output function @{ML \<open>output\<close> in
-  Document_Antiquotation} in the next line pretty prints the code. This function expects
-  that the code is a list of (pretty)strings where each string correspond to a
-  line in the output. Therefore the use of @{ML \<open>(space_explode "\\n" txt)\<close>
-  for txt} which produces such a list according to linebreaks.  There are a
+  ``approved'' by the compiler, then the output given to @{ML \<open>antiquotation_pretty_source\<close> in
+  Thy_Output} in the Line 15 pretty prints the code. This function expects
+  that the code is (pretty) string. There are a
   number of options for antiquotations that are observed by the function 
   @{ML \<open>output\<close> in Document_Antiquotation} when printing the code (including \<open>[display]\<close> 
-  and \<open>[quotes]\<close>). The function @{ML \<open>antiquotation_raw\<close> in Thy_Output} in 
-  Line 7 sets up the new document antiquotation.
+  and \<open>[quotes]\<close>). 
 
   \begin{readmore}
   For more information about options of document antiquotations see \rsccite{sec:antiq}).
   \end{readmore}
 
-  Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific 
-  information about the line number, in case an error is detected. We 
-  can improve the code above slightly by writing 
 \<close>
 
 text \<open>
-  where in Lines 1 and 2 the positional information is properly treated. The
-  parser @{ML Parse.position} encodes the positional information in the 
-  result.
-
-  We can now write \<open>@{ML_checked2 "2 + 3"}\<close> in a document in order to
-  obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
-  somebody changes the definition of addition.
-
-
   The second document antiquotation we describe extends the first by a pattern
   that specifies what the result of the ML-code should be and checks the
   consistency of the actual result with the given pattern. For this we are
@@ -105,11 +90,7 @@
   give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close>
   for specifying a pair.  In order to check consistency between the pattern
   and the output of the code, we have to change the ML-expression that is sent 
-  to the compiler: in \<open>ML_checked2\<close> we sent the expression @{text [quotes]
-  "val _ = a_piece_of_code"} to the compiler; now the wildcard \<open>_\<close>
-  must be be replaced by the given pattern. However, we have to remove all
-  ellipses from it and replace them by @{text [quotes] "_"}. The following 
-  function will do this:
+  to the compiler: 
 \<close>
 
 ML%linenosgray\<open>fun ml_pat pat code =
@@ -122,7 +103,6 @@
   Next we add a response indicator to the result using:
 \<close>
 
-
 ML %grayML\<open>fun add_resp pat = map (fn s => "> " ^ s) pat\<close>
 
 text \<open>
@@ -151,9 +131,9 @@
 
 (* FIXME *)
 text \<open>
-  In comparison with \<open>ML_checked\<close>, we only changed the line about 
-  the compiler (Line~2), the lines about
-  the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 
+  In comparison with \<open>ML_checked\<close>, we changed the line about 
+  the compiler (Lines 4 to 5), the lines about
+  the output (Lines 6 to 7 and 9) and the parser setup (Line 14). Now 
   you can write
  
   @{text [display] \<open>@{ML_resp [display] "true andalso false" "false"}\<close>}

--- a/ProgTutorial/Solutions.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Wed May 22 13:24:30 2019 +0200
@@ -194,7 +194,7 @@
 end\<close>
 
 text \<open>
-  In Line 11 we apply the rule @{thm [source] impE1} in concjunction 
+  In Line 9 we apply the rule @{thm [source] impE1} in concjunction 
   with @{ML assume_tac} in order to reduce the number of possibilities that
   need to be explored. You can use the tactic as follows.
 \<close>

--- a/ProgTutorial/Tactical.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Wed May 22 13:24:30 2019 +0200
@@ -1724,9 +1724,9 @@
   after one step. In this way, we can split simplification of permutations
   into three phases without the user noticing anything about the auxiliary 
   constant. We first freeze any instance of permutation compositions in the term using 
-  lemma @{thm [source] "perm_aux_expand"} (Line 9);
+  lemma @{thm [source] "perm_aux_expand"} (Line 10);
   then simplify all other permutations including pushing permutations over
-  other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+  other permutations by rule @{thm [source] perm_compose_aux} (Line 11); and
   finally ``unfreeze'' all instances of permutation compositions by unfolding 
   the definition of the auxiliary constant. 
 \<close>
@@ -1800,8 +1800,7 @@
 
 text \<open>
   This function takes a simpset and a redex (a @{ML_type cterm}) as
-  arguments. In Lines 3 and~4, we first extract the context from the given
-  simpset and then print out a message containing the redex.  The function
+  arguments and prints out a message containing the redex.  The function
   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
   moment we are \emph{not} interested in actually rewriting anything. We want
   that the simproc is triggered by the pattern @{term "Suc n"}. This can be
@@ -2518,15 +2517,15 @@
   Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
   first transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
   import these variables into the context \<open>ctxt'\<close>, in order to
-  export them again in Line 15.  In Line 8 we certify the list of variables,
+  export them again in Line 14.  In Line 7 we certify the list of variables,
   which in turn we apply to the @{ML_text lhs} of the definition using the
-  function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the
+  function @{ML_ind list_comb in Drule}. In Line 10 and 11 we generate the
   conversion according to the length of the list of (abstracted) variables. If
   there are none, then we just return the conversion corresponding to the
   original definition. If there are variables, then we have to prefix this
-  conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to
+  conversion with @{ML_ind fun_conv in Conv}. Now in Line 13 we only have to
   apply the new left-hand side to the generated conversion and obtain the the
-  theorem we want to construct. As mentioned above, in Line 15 we only have to
+  theorem we want to construct. As mentioned above, in Line 14 we only have to
   export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 
   produce meta-variables for the theorem.  An example is as follows.