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