diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jul 08 11:34:10 2014 +0100
@@ -31,6 +31,9 @@
 fun ml_type txt = 
   implode ["val _ = NONE : (", txt, ") option"];
 
+fun ml_out txt =
+  implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""]
+
 (* eval function *)
 fun eval_fn ctxt exp =
   ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags 
@@ -82,18 +85,18 @@
 (* 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);*)
+     eval_fn ctxt (ml_out lhs);
      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);*)
+     eval_fn ctxt (ml_out lhs);
      output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = 
-    output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))
+    (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 val single_arg = Scan.lift (Args.name)
 val two_args   = Scan.lift (Args.name -- Args.name)