# HG changeset patch
# User haftmann
# Date 1251807214 -7200
# Node ID 87201c60ae7dae1a9a650fb18c19048d39c5c2ee
# Parent  b928f2948bf58fecd03c377156ad0e45be8bb35c# Parent  8ca2f3500dbcc9f5902ed79b30cc94ab84ca2c1d
merged

diff -r 8ca2f3500dbc -r 87201c60ae7d src/HOL/Tools/transfer_data.ML
--- 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;
 
diff -r 8ca2f3500dbc -r 87201c60ae7d src/Pure/General/alist.ML
--- 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;