1.1 --- a/src/Pure/Isar/method.ML	Fri Jul 27 21:55:19 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Jul 27 21:55:20 2007 +0200
     1.3 @@ -465,13 +465,11 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun sect ss = Scan.first (map Scan.lift ss);
     1.8 -fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> flat;
     1.9 -
    1.10 +fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
    1.11  fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
    1.12  
    1.13 -fun section ss = (sect ss -- thms ss) :-- (fn (m, ths) => Scan.depend (fn context =>
    1.14 -  Scan.succeed (app m (context, ths)))) >> #2;
    1.15 +fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :--
    1.16 +  (fn (m, ths) => Scan.succeed (app m (context, ths))) >> #2);
    1.17  
    1.18  fun sectioned args ss = args -- Scan.repeat (section ss);
    1.19