src/Pure/Isar/method.ML
changeset 24022 ab76c73b3b58
parent 24010 2ef318813e1a
child 24116 9915c39e0820
     1.1 --- a/src/Pure/Isar/method.ML	Sat Jul 28 20:40:26 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Jul 28 20:40:27 2007 +0200
     1.3 @@ -468,8 +468,8 @@
     1.4  fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
     1.5  fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
     1.6  
     1.7 -fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :--
     1.8 -  (fn (m, ths) => Scan.succeed (app m (context, ths))) >> #2);
     1.9 +fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
    1.10 +  (fn (m, ths) => Scan.succeed (app m (context, ths))));
    1.11  
    1.12  fun sectioned args ss = args -- Scan.repeat (section ss);
    1.13