src/Pure/Isar/class.ML

           maps (fn (_, ts_pss) => map
             (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
       | check_element e = [()];
     val _ = map check_element syntax_elems;
     fun fork_syn (Element.Fixes xs) =
-          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
+          fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
       (K (TFree (Name.aT, base_sort))) supparams);

       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     val all_params = Locale.params_of thy class;
     val raw_params = (snd o chop (length supparams)) all_params;
     fun add_const (b, SOME raw_ty, _) thy =
       let
-        val v = Binding.base_name b;
+        val v = Binding.name_of b;
         val c = Sign.full_bname thy v;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
         val ty0 = Type.strip_sorts ty;
         val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
         val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;

   in
     thy
     |> add_consts bname class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
-          [((Binding.empty, []),
-            Option.map (globalize param_map) raw_pred |> the_list)]
+          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
     #> pair (param_map, params, assm_axiom)))
   end;