diff -r b210ae666a42 -r a849ce33923d src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Aug 04 08:12:54 2017 +0200
@@ -199,15 +199,16 @@
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init (Sign.naming_of thy)
+    |> Local_Theory.init
+       {background_naming = Sign.naming_of thy,
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in overloading target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);