# HG changeset patch
# User wenzelm
# Date 1085167158 -7200
# Node ID 4f3b383a46aee7af103ee777334c5ef8907cddf7
# Parent  65c22319829f0ad3321d28f866ac41a92bbe7ad1
Args.local_typ_raw;

diff -r 65c22319829f -r 4f3b383a46ae src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri May 21 21:19:04 2004 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri May 21 21:19:18 2004 +0200
@@ -335,7 +335,7 @@
  [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
-  ("typ", args Args.local_typ_no_norm (output_with ProofContext.pretty_typ)),
+  ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("goals", output_goals true),
   ("subgoals", output_goals false),