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