src/HOL/Tools/old_primrec.ML

 (*the following code ensures that each recursive set always has the
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
   (let
     fun varify t (i, ts) =
-      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
+      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
       in (maxidx_of_term t', t'::ts) end;
     val (i, cs') = fold_rev varify cs (~1, []);
     val (i', intr_ts') = fold_rev varify intr_ts (i, []);
     val rec_consts = fold Term.add_consts cs' [];
     val intr_consts = fold Term.add_consts intr_ts' [];

         (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
     val (simps', thy'') =
       thy'
       |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     val simps'' = maps snd simps';
-    val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
+    val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
   in
     thy''
     |> note (("simps",
         [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
     |> snd