--- a/src/Pure/Isar/overloading.ML Tue Mar 31 11:39:24 2015 +0200
+++ b/src/Pure/Isar/overloading.ML Tue Mar 31 11:56:21 2015 +0200
@@ -189,7 +189,6 @@
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)));
@@ -201,7 +200,7 @@
|> 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,