# HG changeset patch
# User wenzelm
# Date 1118311412 -7200
# Node ID b035482bed0226316a3261fa48c72a3109ea6530
# Parent  a52fe1277902b57879bd3f3abf5d72739f72164f
Args.local_typ_abbrev;

diff -r a52fe1277902 -r b035482bed02 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Thu Jun 09 12:03:31 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Thu Jun 09 12:03:32 2005 +0200
@@ -399,7 +399,7 @@
   ("term_type", args Args.local_term (output_with pretty_term_typ)),
   ("typeof", args Args.local_term (output_with pretty_term_typeof)),
   ("const", args Args.local_term (output_with pretty_term_const)),
-  ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
+  ("typ", args Args.local_typ_abbrev (output_with ProofContext.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("goals", output_goals true),
   ("subgoals", output_goals false),