--- a/src/HOL/Tools/transfer_data.ML Tue Sep 01 14:10:38 2009 +0200
+++ b/src/HOL/Tools/transfer_data.ML Tue Sep 01 14:13:34 2009 +0200
@@ -223,7 +223,8 @@
transf_add
>> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
-val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term)) -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
+val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
+ -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
end;
--- a/src/Pure/General/alist.ML Tue Sep 01 14:10:38 2009 +0200
+++ b/src/Pure/General/alist.ML Tue Sep 01 14:13:34 2009 +0200
@@ -122,6 +122,6 @@
in coal end;
fun group eq xs =
- fold_rev (fn (k, v) => default eq (k, []) #> map_entry eq k (cons v)) xs [];
+ fold_rev (fn (k, v) => map_default eq (k, []) (cons v)) xs [];
end;