src/Pure/Isar/attrib.ML
changeset 30240 5b25fee0362c
parent 29690 c81f8b2967e1
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -118,8 +118,7 @@
     1.4  fun attribute thy = attribute_i thy o intern_src thy;
     1.5  
     1.6  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     1.7 -    [((Binding.empty, []),
     1.8 -      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
     1.9 +    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.10    |> fst |> maps snd;
    1.11  
    1.12  
    1.13 @@ -198,7 +197,7 @@
    1.14        let
    1.15          val ths = Facts.select thmref fact;
    1.16          val atts = map (attribute_i thy) srcs;
    1.17 -        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
    1.18 +        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
    1.19        in (context', pick name ths') end)
    1.20    end);
    1.21