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