--- a/ProgTutorial/antiquote_setup.ML	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Mon Apr 30 14:43:52 2012 +0100
@@ -81,13 +81,13 @@
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
-     write_file_ml_blk lhs (Proof_Context.theory_of ctxt);
+     (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE lhs);
-     write_file_ml_blk lhs (Proof_Context.theory_of ctxt);
+     (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
      output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)