src/Pure/Isar/proof_context.ML
changeset 18418 bf448d999b7e
parent 18375 99deeed095ae
child 18428 4059413acbc1
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -1018,7 +1018,7 @@
     1.4  fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
     1.5    let
     1.6      fun app (th, attrs) (ct, ths) =
     1.7 -      let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
     1.8 +      let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th)
     1.9        in (ct', th' :: ths) end;
    1.10      val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
    1.11      val thms = List.concat (rev rev_thms);