Moved unify_consts to PrimrecPackage.
authorberghofe
Wed Jul 11 11:34:38 2007 +0200 (2007-07-11)
changeset 23758705f25072f5c
parent 23757 087b0a241557
child 23759 90bccef65004
Moved unify_consts to PrimrecPackage.
src/HOL/Nominal/nominal_primrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jul 11 11:32:02 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jul 11 11:34:38 2007 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
     1.5        (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
     1.6        handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
     1.7 -    val (_, eqn_ts') = OldInductivePackage.unify_consts thy rec_ts eqn_ts
     1.8 +    val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts
     1.9    in
    1.10      gen_primrec_i note def alt_name
    1.11        (Option.map (map (readt dummyT)) invs)