src/ZF/Tools/inductive_package.ML

 
   (*Big_rec... is the union of the mutually recursive sets*)
   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*)
            | _ => rec_tms ~~          (*define the sets as Parts*)
                   map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));