src/Pure/Isar/proof_context.ML
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 30211 556d1810cdad
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -975,7 +975,7 @@
     1.4  
     1.5      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
     1.6      fun app (th, attrs) x =
     1.7 -      swap (foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
     1.8 +      swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
     1.9      val (res, ctxt') = fold_map app facts ctxt;
    1.10      val thms = PureThy.name_thms false false pos name (flat res);
    1.11      val Mode {stmt, ...} = get_mode ctxt;