Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add_abbrevs: unvarify result;
authorwenzelm
Sat, 13 Oct 2007 17:16:42 +0200
changeset 25019 3b2d3b8fc7b6
parent 25018 fac2ceba75b4
child 25020 f1344290e420
add_abbrevs: unvarify result;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle