src/Pure/Thy/thy_output.ML
changeset 26710 f79aa228c582
parent 26455 1757a6e049f4
child 26762 78ed28528ca6
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Apr 17 16:30:55 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Apr 17 22:22:19 2008 +0200
     1.3 @@ -429,10 +429,9 @@
     1.4  
     1.5  val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
     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  
    1.10 -fun pretty_term_abbrev ctxt =
    1.11 -  ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
    1.12 +fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t;
    1.13  
    1.14  fun pretty_term_typ ctxt t =
    1.15    Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);