1.1 --- a/doc-src/antiquote_setup.ML	Thu Apr 17 16:30:55 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu Apr 17 22:22:19 2008 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4      #> space_implode "\\par\\smallskip%\n"
     1.5      #> enclose "\\isa{" "}");
     1.6  
     1.7 -fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.8 +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
     1.9  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.10  
    1.11  in

     2.1 --- a/src/Pure/Thy/thy_output.ML	Thu Apr 17 16:30:55 2008 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Apr 17 22:22:19 2008 +0200
     2.3 @@ -429,10 +429,9 @@
     2.4  
     2.5  val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
     2.6  
     2.7 -fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     2.8 +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
     2.9  
    2.10 -fun pretty_term_abbrev ctxt =
    2.11 -  ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
    2.12 +fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t;
    2.13  
    2.14  fun pretty_term_typ ctxt t =
    2.15    Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);