avoid long line
authorhaftmann
Mon, 24 Aug 2009 08:31:41 +0200
changeset 324750d7e8d858b44
parent 32394 e8feef03a93f
child 32476 b928f2948bf5
avoid long line
src/HOL/Tools/transfer_data.ML
     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