equal
deleted
inserted
replaced
116 in attr end; |
116 in attr end; |
117 |
117 |
118 fun attribute thy = attribute_i thy o intern_src thy; |
118 fun attribute thy = attribute_i thy o intern_src thy; |
119 |
119 |
120 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
120 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
121 [((Binding.empty, []), |
121 [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt |
122 map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt |
|
123 |> fst |> maps snd; |
122 |> fst |> maps snd; |
124 |
123 |
125 |
124 |
126 (* attributed declarations *) |
125 (* attributed declarations *) |
127 |
126 |