--- a/ProgTutorial/Parsing.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Parsing.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -1160,7 +1160,7 @@
     let
       val prop = Syntax.read_prop lthy str
     in
-      Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
+      Proof.theorem NONE (K I) [[(prop, [])]] lthy
     end
   
   val kind = OuterKeyword.thy_goal
@@ -1173,7 +1173,7 @@
   The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context as argument.  The context is necessary in order to be able to use
   @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
-  In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the
+  In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
   proposition. Its argument @{ML NONE} stands for a locale (which we chose to
   omit); the argument @{ML "(K I)"} stands for a function that determines what
   should be done with the theorem once it is proved (we chose to just forget
@@ -1211,7 +1211,7 @@
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end
 
    val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source