# HG changeset patch
# User wenzelm
# Date 1208463739 -7200
# Node ID f79aa228c582a1a13ad053a05bc16d0171149b12
# Parent  f963ea18a579390ec1ec88ab05cedee1a8ae6455
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);

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
diff -r f963ea18a579 -r f79aa228c582 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Apr 17 16:30:55 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Apr 17 22:22:19 2008 +0200
@@ -429,10 +429,9 @@
 
 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
 
-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_term_abbrev ctxt =
-  ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t;
 
 fun pretty_term_typ ctxt t =
   Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);