--- a/ProgTutorial/antiquote_setup.ML	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Wed Oct 26 12:59:44 2011 +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 (ProofContext.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 (ProofContext.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 *)