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