changeset 8819 | d04923e183c7 |
parent 8438 | b8389b4fca9c |
child 9179 | 44eabc57ed46 |
8818:253dad743f00 | 8819:d04923e183c7 |
---|---|
189 in |
189 in |
190 (thy'', char_thms) |
190 (thy'', char_thms) |
191 end; |
191 end; |
192 |
192 |
193 fun add_primrec eqns thy = |
193 fun add_primrec eqns thy = |
194 add_primrec_i (map (apsnd (readtm (sign_of thy) propT)) eqns) thy; |
194 add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy; |
195 |
195 |
196 end; |
196 end; |