--- a/src/HOL/Tools/legacy_transfer.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML Sun Oct 18 21:30:01 2015 +0200
@@ -217,7 +217,7 @@
|| keyword_colon congN || keyword_colon labelsN
|| keyword_colon leavingN || keyword_colon directionN;
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)