src/Pure/Isar/proof_context.ML

 local
 
 fun prep_vars prep_typ internal =
   fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     let
-      val raw_x = Name.name_of raw_b;
+      val raw_x = Binding.base_name raw_b;
       val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
       val _ = Syntax.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ quote x);
 
       fun cond_tvars T =

   else (true, (x, T, mx));
 
 fun gen_fixes prep raw_vars ctxt =
   let
     val (vars, _) = prep raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
+    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>