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