more robust pretty_term_typ, using well-typed parse tree representation;

--- 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;