src/Pure/Thy/thy_output.ML
changeset 24680 0d355aa59e67
parent 23942 079e99db59d7
child 24920 2a45e400fdad
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Sep 23 22:23:24 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Sep 23 22:23:27 2007 +0200
     1.3 @@ -434,7 +434,7 @@
     1.4    ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
     1.5  
     1.6  fun pretty_term_typ ctxt t =
     1.7 -  ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
     1.8 +  ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
     1.9  
    1.10  fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
    1.11