doc-src/more_antiquote.ML

--- a/doc-src/more_antiquote.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/doc-src/more_antiquote.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -27,7 +27,7 @@
 
 fun pretty_code_thm src ctxt raw_const =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
     val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];