# HG changeset patch
# User wenzelm
# Date 1192288602 -7200
# Node ID 3b2d3b8fc7b6fd9c2dc40d99199184a3903bdaa8
# Parent  fac2ceba75b4be973ff39f5ebfb9260aca99eb82
add_abbrevs: unvarify result;

diff -r fac2ceba75b4 -r 3b2d3b8fc7b6 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Oct 13 17:16:41 2007 +0200
+++ b/src/Pure/sign.ML	Sat Oct 13 17:16:42 2007 +0200
@@ -714,7 +714,7 @@
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val (res, consts') = consts_of thy
       |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
-  in (res, thy |> map_consts (K consts')) end;
+  in (pairself Logic.unvarify res, thy |> map_consts (K consts')) end;
 
 
 (* add constraints *)