# HG changeset patch
# User wenzelm
# Date 1192547180 -7200
# Node ID b15a9a5dc9fe4a4f0a08ce3436c249d3b6ac7274
# Parent  2b86fac03ec5e53d1f72457585eece98ad05ea5f
tuned Const.the_abbreviation;

diff -r 2b86fac03ec5 -r b15a9a5dc9fe src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Oct 16 17:06:19 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 16 17:06:20 2007 +0200
@@ -448,7 +448,7 @@
     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 ();
-    val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
+    val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
       handle TYPE _ => err ();
     val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;