tuned;

--- a/src/Pure/Isar/class.ML	Tue Mar 31 11:39:24 2015 +0200
+++ b/src/Pure/Isar/class.ML	Tue Mar 31 11:56:21 2015 +0200
@@ -599,8 +599,6 @@
 
 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))) =
@@ -637,7 +635,7 @@
     |> 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,

--- a/src/Pure/Isar/named_target.ML	Tue Mar 31 11:39:24 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Mar 31 11:56:21 2015 +0200
@@ -155,8 +155,8 @@
 fun gen_init before_exit target thy =
   let
     val name_data = make_name_data thy target;
-    val naming = Sign.naming_of thy
-      |> Name_Space.mandatory_path (Long_Name.base_name target);
+    val naming =
+      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
     thy
     |> Sign.change_begin

--- 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,