diff -r 8fe7414f00b1 -r 4d46d53566e6 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Tue Mar 11 21:58:41 2014 +0100
+++ b/src/Pure/Isar/overloading.ML	Tue Mar 11 22:49:28 2014 +0100
@@ -194,6 +194,7 @@
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy
+    |> Sign.change_begin
     |> Proof_Context.init_global
     |> Data.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
@@ -205,7 +206,7 @@
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
-        exit = Local_Theory.target_of o conclude}
+        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);