| changeset 42361 | 23f352990944 |
| parent 41532 | 0d34deffb0e9 |
| child 43564 | 9864182c6bad |
--- 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)