--- 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 *)