diff -r c8a9a5e577bd -r ac069060e08a src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Nov 10 17:41:36 2011 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Nov 10 17:47:25 2011 +0100
@@ -114,8 +114,8 @@
 
 val activate_improvable_syntax =
   Context.proof_map
-    (Syntax_Phases.context_term_check 0 "improvement" improve_term_check
-    #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck)
+    (Syntax_Phases.term_check' 0 "improvement" improve_term_check
+    #> Syntax_Phases.term_uncheck' 0 "improvement" improve_term_uncheck)
   #> set_primary_constraints;