src/Pure/Isar/attrib.ML
changeset 30761 ac7570d80c3d
parent 30759 3bc78fbb9f57
child 31174 f1f1e9b53c81
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 28 17:10:43 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 28 17:21:11 2009 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5  fun attribute thy = attribute_i thy o intern_src thy;
     1.6  
     1.7 -fun eval_thms ctxt args = ProofContext.note_thmss_i Thm.theoremK
     1.8 +fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     1.9      [(Thm.empty_binding, args |> map (fn (a, atts) =>
    1.10          (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
    1.11    |> fst |> maps snd;