# HG changeset patch
# User wenzelm
# Date 1303162875 -7200
# Node ID 95b17b4901b562f6916b60fc4bc307f3325a8598
# Parent  919e17c0358e0c9a403b923b5a76a8c5309f551e
pretty_abbrev: read abbreviation more directly;

diff -r 919e17c0358e -r 95b17b4901b5 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Apr 18 20:40:31 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Apr 18 23:41:15 2011 +0200
@@ -498,7 +498,7 @@
 
 fun pretty_abbrev ctxt s =
   let
-    val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt);
+    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
     fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
     val (head, args) = Term.strip_comb t;
     val (c, T) = Term.dest_Const head handle TERM _ => err ();