src/HOL/Tools/inductive_realizer.ML

         let
           val Const (s, T) = head_of (HOLogic.dest_Trueprop
             (Logic.strip_assums_concl rintr));
           val s' = Sign.base_name s;
           val T' = Logic.unvarifyT T
-        in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
     val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
       (List.take (snd (strip_comb
         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
 
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
-        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
+        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
           coind = false, no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
-          ((Name.binding (Sign.base_name (name_of_thm intr)), []),
+          ((Binding.name (Sign.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
              (rintrs ~~ maps snd rss)) [] ||>
       Sign.absolute_path;
     val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';