src/Pure/Isar/attrib.ML
changeset 28083 103d9282a946
parent 27865 27a8ad9612a3
child 28084 a05ca48ef263
--- a/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:45 2008 +0200
@@ -110,7 +110,8 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+    [((Name.no_binding, []),
+      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   |> fst |> maps snd;