1.1 --- a/src/HOL/Tools/transfer_data.ML Sat Aug 22 23:22:17 2009 +0200
1.2 +++ b/src/HOL/Tools/transfer_data.ML Mon Aug 24 08:31:41 2009 +0200
1.3 @@ -223,7 +223,8 @@
1.4 transf_add
1.5 >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
1.6
1.7 -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));
1.8 +val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
1.9 + -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
1.10
1.11 end;
1.12