changeset 31177 | c39994cb152a |
parent 31174 | f1f1e9b53c81 |
child 31305 | a16f4d4f5b24 |
--- a/src/Pure/Isar/attrib.ML Sun May 17 07:17:39 2009 +0200 +++ b/src/Pure/Isar/attrib.ML Mon May 18 09:48:06 2009 +0200 @@ -123,7 +123,7 @@ fun attribute thy = attribute_i thy o intern_src thy; -fun eval_thms ctxt args = ProofContext.note_thmss Thm.generated_theoremK +fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK [(Thm.empty_binding, args |> map (fn (a, atts) => (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt |> fst |> maps snd;