| changeset 61476 | 1884c40f1539 |
| parent 61268 | abe08fb15a12 |
| child 61812 | 71446a608dfd |
--- a/src/Pure/Isar/method.ML Sun Oct 18 20:48:24 2015 +0200 +++ b/src/Pure/Isar/method.ML Sun Oct 18 21:30:01 2015 +0200 @@ -526,7 +526,7 @@ local fun thms ss = - Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; + Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm); fun app {init, attribute, pos = _} ths context = fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context);