--- 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)),