src/Pure/Isar/class.ML

       else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco)));
   in lthy end;
 
 fun instantiation (tycos, vs, sort) thy =
   let
-    val naming = Sign.naming_of thy;
-
     val _ = if null tycos then error "At least one arity must be given" else ();
     val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
       if can (Axclass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),

     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_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,