# HG changeset patch
# User berghofe
# Date 939130336 -7200
# Node ID 8add8fdce3f1f6740492c5245adfd1d7a7bb458f
# Parent  cb353d802adef65b38227142bc5cfc3f217d35e8
Got rid of readtm.

diff -r cb353d802ade -r 8add8fdce3f1 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Tue Oct 05 15:31:42 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Tue Oct 05 15:32:16 1999 +0200
@@ -262,7 +262,7 @@
     val sign = Theory.sign_of thy;
     val ((names, strings), srcss) = apfst split_list (split_list eqns);
     val atts = map (map (Attrib.global_attribute thy)) srcss;
-    val eqn_ts = map (readtm sign propT) strings;
+    val eqn_ts = map (term_of o Thm.read_cterm sign o rpair propT) strings;
     val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
       handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts;
     val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts