# HG changeset patch
# User wenzelm
# Date 1146859189 -7200
# Node ID 4ae6a14b742f1f01486dcc1a2b2c8ad1511d09fd
# Parent  c878a09fb8497f7f981b1b698f70a6ec7fd84d45
more robust pretty_term_typ, using well-typed parse tree representation;

diff -r c878a09fb849 -r 4ae6a14b742f src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri May 05 21:59:48 2006 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri May 05 21:59:49 2006 +0200
@@ -439,10 +439,7 @@
 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
 
 fun pretty_term_typ ctxt t =
-  (Syntax.const Syntax.constrainC $
-    ProofContext.extern_skolem ctxt t $
-    Syntax.term_of_typ (! show_sorts) (Term.fastype_of t))
-  |> ProofContext.pretty_term ctxt;
+  ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
 
 fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;