--- 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);