--- a/src/Pure/Isar/attrib.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Oct 18 21:30:01 2015 +0200
@@ -281,7 +281,7 @@
val thm = gen_thm Facts.the_single;
val multi_thm = gen_thm (K I);
-val thms = Scan.repeat multi_thm >> flat;
+val thms = Scan.repeats multi_thm;
end;