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