equal
deleted
inserted
replaced
108 in attr end; |
108 in attr end; |
109 |
109 |
110 fun attribute thy = attribute_i thy o intern_src thy; |
110 fun attribute thy = attribute_i thy o intern_src thy; |
111 |
111 |
112 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
112 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK |
113 [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt |
113 [((Name.no_binding, []), |
|
114 map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt |
114 |> fst |> maps snd; |
115 |> fst |> maps snd; |
115 |
116 |
116 |
117 |
117 (* attributed declarations *) |
118 (* attributed declarations *) |
118 |
119 |