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;