--- a/ProgTutorial/antiquote_setup.ML	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Oct 13 22:57:25 2009 +0200
@@ -81,11 +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 (Context.theory_of_proof ctxt);
      output ((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 (Context.theory_of_proof ctxt);
      output ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)