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*)