src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:43 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;