changeset 24920 | 2a45e400fdad |
parent 24584 | 01e83ffa6c54 |
child 26385 | ae7564661e76 |
--- a/doc-src/antiquote_setup.ML Mon Oct 08 22:06:32 2007 +0200 +++ b/doc-src/antiquote_setup.ML Tue Oct 09 00:20:13 2007 +0200 @@ -76,7 +76,7 @@ #> space_implode "\\par\\smallskip%\n" #> enclose "\\isa{" "}"); -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt; +fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; in