tuned Const.the_abbreviation;

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