src/ZF/Tools/inductive_package.ML
changeset 35989 3418cdf1855e
parent 35409 5c5bb83f2bae
child 36541 de1862c4a308
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 27 17:36:32 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 27 18:07:21 2010 +0100
@@ -156,7 +156,7 @@
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
-  val axpairs = map Primitive_Defs.mk_defpair
+  val axpairs = map OldGoals.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)