diff -r 3633f560f4c3 -r 479806475f3c src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Mar 01 16:48:06 2009 +0100 +++ b/src/Pure/Isar/method.ML Sun Mar 01 23:36:12 2009 +0100 @@ -436,7 +436,7 @@ local fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; -fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths); +fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths); fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- (fn (m, ths) => Scan.succeed (app m (context, ths))));