| changeset 8819 | d04923e183c7 |
| parent 8438 | b8389b4fca9c |
| child 9179 | 44eabc57ed46 |
--- a/src/ZF/Tools/primrec_package.ML Fri May 05 22:35:51 2000 +0200 +++ b/src/ZF/Tools/primrec_package.ML Fri May 05 22:37:04 2000 +0200 @@ -191,6 +191,6 @@ end; fun add_primrec eqns thy = - add_primrec_i (map (apsnd (readtm (sign_of thy) propT)) eqns) thy; + add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy; end;