src/HOL/Nominal/nominal_primrec.ML

     val eqn_ts = map (fn s => Syntax.read_prop_global thy s
       handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
     val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
       (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
       handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
-    val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts
+    val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts
   in
     gen_primrec_i note def alt_name
       (Option.map (map (Syntax.read_term_global thy)) invs)
       (Option.map (Syntax.read_term_global thy) fctxt)
       (names ~~ eqn_ts' ~~ atts) thy