diff -r f963ea18a579 -r f79aa228c582 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Thu Apr 17 16:30:55 2008 +0200 +++ b/doc-src/antiquote_setup.ML Thu Apr 17 22:22:19 2008 +0200 @@ -83,7 +83,7 @@ #> space_implode "\\par\\smallskip%\n" #> enclose "\\isa{" "}"); -fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt; +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; in