src/Pure/Isar/overloading.ML

   in lthy end;
 
 fun gen_overloading prep_const raw_overloading thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val naming = Sign.naming_of thy;
     val _ = if null raw_overloading then error "At least one parameter must be given" else ();
     val overloading = raw_overloading |> map (fn (v, const, checked) =>
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy

     |> Proof_Context.init_global
     |> Data.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init naming
+    |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,