diff -r 253dad743f00 -r d04923e183c7 src/ZF/Tools/primrec_package.ML
--- 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;