# HG changeset patch # User berghofe # Date 1184147819 -7200 # Node ID 742be2833ccd680f21b71fc7d0e3bca3a19122dc # Parent 18f426a137a95da28dbf0e279707f06b0ae5a854 Function unify_consts moved from OldInductivePackage to PrimrecPackage. diff -r 18f426a137a9 -r 742be2833ccd src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Wed Jul 11 11:54:21 2007 +0200 +++ b/src/HOLCF/Tools/fixrec_package.ML Wed Jul 11 11:56:59 2007 +0200 @@ -231,7 +231,7 @@ val eqn_ts = map (prep_prop thy) strings; val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq))) handle TERM _ => fixrec_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; fun unconcat [] _ = [] | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));