diff -r 034150db9d91 -r c3dbc04471a9 ProgTutorial/First_Steps.thy --- 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 \term_pat_setup\ text \ - 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: