Function unify_consts moved from OldInductivePackage to PrimrecPackage.
authorberghofe
Wed, 11 Jul 2007 11:56:59 +0200
changeset 23779 742be2833ccd
parent 23778 18f426a137a9
child 23780 a0e7305dd0cb
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
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));