# HG changeset patch
# User wenzelm
# Date 1332409771 -3600
# Node ID 6231adc3895d8af404af8d840d1285cb09d31fb2
# Parent  6890c02c4c120bf4d1b90423912cfdbbc493a129
synchronize syntax uniformly for target stack and aux. context;

diff -r 6890c02c4c12 -r 6231adc3895d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Mar 22 10:10:30 2012 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 22 10:49:31 2012 +0100
@@ -319,8 +319,8 @@
 fun target_extension f class lthy =
   lthy
   |> Local_Theory.raw_theory f
-  |> Local_Theory.target (synchronize_class_syntax [class]
-      (base_sort (Proof_Context.theory_of lthy) class));
+  |> Local_Theory.map_contexts
+      (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
 
 fun target_const class ((c, mx), (type_params, dict)) thy =
   let
@@ -484,7 +484,7 @@
   Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
   ##>> AxClass.define_overloaded b_def (c, rhs))
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
-  ##> Local_Theory.target synchronize_inst_syntax;
+  ##> Local_Theory.map_contexts synchronize_inst_syntax;
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   (case instantiation_param lthy b of
diff -r 6890c02c4c12 -r 6231adc3895d src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Mar 22 10:10:30 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Mar 22 10:49:31 2012 +0100
@@ -155,7 +155,7 @@
       (Thm.def_binding_optional (Binding.name v) b_def,
         Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
-  ##> Local_Theory.target synchronize_syntax
+  ##> Local_Theory.map_contexts synchronize_syntax
   #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =