src/HOL/Tools/transfer_data.ML
changeset 32476 0d7e8d858b44
parent 31794 71af1fd6a5e4
--- a/src/HOL/Tools/transfer_data.ML	Sat Aug 22 23:22:17 2009 +0200
+++ b/src/HOL/Tools/transfer_data.ML	Mon Aug 24 08:31:41 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;