add_abbrevs: unvarify result;
authorwenzelm
Sat Oct 13 17:16:42 2007 +0200 (2007-10-13)
changeset 250193b2d3b8fc7b6
parent 25018 fac2ceba75b4
child 25020 f1344290e420
add_abbrevs: unvarify result;
src/Pure/sign.ML
     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 *)