diff -r a7f85074c169 -r ff1770df59b8 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 01 09:12:03 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 01 14:29:22 2012 +0200
@@ -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.map_contexts synchronize_syntax
+  ##> Local_Theory.map_contexts (K synchronize_syntax)
   #-> (fn (_, def) => pair (Const (c, U), def));
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =