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