
diff -r da8817d01e7c -r 23f352990944 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Sat Apr 16 15:47:52 2011 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Sat Apr 16 16:15:37 2011 +0200
@@ -5,7 +5,7 @@
 
 ML {*
 fun pretty_term_type_only ctxt (t, T) =
-  (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
+  (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
    else error "term_type_only: type mismatch";
    Syntax.pretty_typ ctxt T)
 




