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