diff -r c0481c3c2a6c -r 6523a21076a8 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 01 19:07:32 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 01 20:36:33 2012 +0200
@@ -203,8 +203,7 @@
     |> synchronize_syntax
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),