equal
deleted
inserted
replaced
121 end; |
121 end; |
122 in attr end; |
122 in attr end; |
123 |
123 |
124 fun attribute thy = attribute_i thy o intern_src thy; |
124 fun attribute thy = attribute_i thy o intern_src thy; |
125 |
125 |
126 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
126 fun eval_thms ctxt args = ProofContext.note_thmss Thm.generated_theoremK |
127 [(Thm.empty_binding, args |> map (fn (a, atts) => |
127 [(Thm.empty_binding, args |> map (fn (a, atts) => |
128 (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt |
128 (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt |
129 |> fst |> maps snd; |
129 |> fst |> maps snd; |
130 |
130 |
131 |
131 |