# HG changeset patch
# User berghofe
# Date 1184146478 -7200
# Node ID 705f25072f5c5d10ab71359d2e8adbbe498f07d5
# Parent  087b0a2415570a74bd728ad8153390e167cd8b08
Moved unify_consts to PrimrecPackage.

diff -r 087b0a241557 -r 705f25072f5c src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jul 11 11:32:02 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jul 11 11:34:38 2007 +0200
@@ -388,7 +388,7 @@
     val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
       (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
       handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
-    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
+    val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts
   in
     gen_primrec_i note def alt_name
       (Option.map (map (readt dummyT)) invs)