src/ZF/Tools/inductive_package.ML
changeset 33385 fb2358edcfb6
parent 33368 b1cf34f1855c
child 35021 c839a4c670c6
--- a/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:38:46 2009 +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 PrimitiveDefs.mk_defpair
+  val axpairs = map Primitive_Defs.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)