src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -118,8 +118,7 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-    [((Binding.empty, []),
-      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   |> fst |> maps snd;
 
 
@@ -198,7 +197,7 @@
       let
         val ths = Facts.select thmref fact;
         val atts = map (attribute_i thy) srcs;
-        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
+        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
       in (context', pick name ths') end)
   end);