# HG changeset patch
# User wenzelm
# Date 1230816219 -3600
# Node ID 8fb76724582236d1bb89e27f9498a468e6baa5c7
# Parent  f45c9c3b40a379216e645ad7674901b5294dca4a
Term.add_consts;

diff -r f45c9c3b40a3 -r 8fb767245822 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -34,14 +34,13 @@
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
   (let
-    val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     fun varify (t, (i, ts)) =
       let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
       in (maxidx_of_term t', t'::ts) end;
     val (i, cs') = foldr varify (~1, []) cs;
     val (i', intr_ts') = foldr varify (i, []) intr_ts;
-    val rec_consts = fold add_term_consts_2 cs' [];
-    val intr_consts = fold add_term_consts_2 intr_ts' [];
+    val rec_consts = fold Term.add_consts cs' [];
+    val intr_consts = fold Term.add_consts intr_ts' [];
     fun unify (cname, cT) =
       let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;