src/ZF/Tools/datatype_package.ML

     kpart is the number of this mutually recursive part*)
   fun mk_con_defs (kpart, con_ty_list) =
     let val ncon = length con_ty_list    (*number of constructors*)
         fun mk_def (((id,T,syn), name, args, prems), kcon) =
               (*kcon is index of constructor*)
-            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
+            OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
                         mk_inject npart kpart
                         (mk_inject ncon kcon (mk_tuple args)))
     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
 
 

   val case_args = maps (map #1) case_lists;
 
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
-  val case_def = Primitive_Defs.mk_defpair
+  val case_def = OldGoals.mk_defpair
     (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
   (** Generating function variables for the recursor definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)

     list_comb (Const (recursor_name, recursor_typ), recursor_args);
 
   val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
 
   val recursor_def =
-      Primitive_Defs.mk_defpair
+      OldGoals.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
            absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)