# HG changeset patch
# User haftmann
# Date 1251095501 -7200
# Node ID 0d7e8d858b44353874d40bc3a45c5c45a5fb785a
# Parent  e8feef03a93f520521deb7729e974096ea124fcc
avoid long line

diff -r e8feef03a93f -r 0d7e8d858b44 src/HOL/Tools/transfer_data.ML
--- 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;