diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/Base.thy	Tue Jun 08 15:18:30 2010 +0200
@@ -104,20 +104,23 @@
       (fn (txt, pos) =>
         Toplevel.generic_theory
          (ML_Context.exec 
-           (fn () => ML_Context.eval true pos txt) 
+           (fn () => ML_Context.eval_text true pos txt) 
               #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
-
+*}
+ML {*
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" 
     (Keyword.tag "TutorialML" Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))
+*}
 
+ML {*
 val _ =
   Outer_Syntax.command "ML_val" "diagnostic ML text" 
   (Keyword.tag "TutorialML" Keyword.diag)
-    (Parse.ML_source >> IsarCmd.ml_diag true)
+    (Parse.ML_source >> Isar_Cmd.ml_diag true)
 *}
 
 ML {*
@@ -125,7 +128,7 @@
   Outer_Syntax.command "setup" "ML theory setup" 
     (Keyword.tag_ml Keyword.thy_decl)
       (Parse.ML_source >> (fn (txt, pos) => 
-        (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
+        (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
 *}
 
 ML {*
@@ -133,7 +136,7 @@
   Outer_Syntax.local_theory "local_setup" "ML local theory setup" 
     (Keyword.tag_ml Keyword.thy_decl)
       (Parse.ML_source >> (fn (txt, pos) => 
-         IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
+         Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}
 
 ML {*