diff -r 42a1c230daff -r 43df2d59fb98 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue Oct 20 12:25:20 2009 +0200 +++ b/ProgTutorial/antiquote_setup.ML Thu Oct 22 02:03:14 2009 +0200 @@ -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 (Context.theory_of_proof ctxt); + write_file_ml_blk lhs (ProofContext.theory_of 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); + write_file_ml_blk lhs (ProofContext.theory_of ctxt); output ((split_lines lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *)