src/Pure/Isar/method.ML
changeset 18418 bf448d999b7e
parent 18309 5ca7ba291f35
child 18474 180c99dfbad4
     1.1 --- a/src/Pure/Isar/method.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -624,7 +624,7 @@
     1.4  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
     1.5  fun thmss ss = Scan.repeat (thms ss) >> List.concat;
     1.6  
     1.7 -fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]);
     1.8 +fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
     1.9  
    1.10  fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    1.11    Scan.succeed (apply m (ctxt, ths)))) >> #2;