src/Pure/Isar/attrib.ML
changeset 33666 e49bfeb0d822
parent 33522 737589bb9bb8
child 34986 7f7939c9370f
--- a/src/Pure/Isar/attrib.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -120,7 +120,7 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
+fun eval_thms ctxt args = ProofContext.note_thmss ""
     [(Thm.empty_binding, args |> map (fn (a, atts) =>
         (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   |> fst |> maps snd;