diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/antiquote_setup.ML --- 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 *)