--- a/ProgTutorial/Helper/Command/Command.thy	Sat Apr 24 22:55:50 2010 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Mon Apr 26 05:20:01 2010 +0200
@@ -29,7 +29,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 prove_prop_parser = OuterParse.prop >> prove_prop
    val kind = OuterKeyword.thy_goal
@@ -51,7 +51,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