diff -r 007922777ff1 -r ee864694315b ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Mon Aug 17 20:57:32 2009 +0200
+++ b/ProgTutorial/Base.thy	Tue Aug 18 01:05:56 2009 +0200
@@ -21,7 +21,7 @@
          val stream = TextIO.openAppend name
        in
          TextIO.output (stream, txt); 
-         TextIO.flushOut stream;
+         TextIO.flushOut stream;                (* needed ?*)
          TextIO.closeOut stream
        end)
 *}
@@ -45,7 +45,6 @@
   (open_file name; write_file (txt ^ "\n"))
 *}
 
-
 ML {*
 
 fun propagate_env (context as Context.Proof lthy) =
@@ -54,27 +53,21 @@
 
 fun propagate_env_prf prf = Proof.map_contexts
   (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
-*}
 
-ML {*
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
     (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
     (OuterParse.position OuterParse.text >> (fn (txt, pos) =>
       Toplevel.generic_theory
         (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env)))
-*}
 
-ML {*
 val _ =
   OuterSyntax.command "ML_prf" "ML text within proof" 
     (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
     (OuterParse.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 {*
 val _ =
   OuterSyntax.command "ML_val" "diagnostic ML text" 
   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)