diff -r ca4cf5de366c -r 392c4cd97e5c src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Tue Apr 03 10:04:41 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Tue Apr 03 10:59:20 2012 +0200
@@ -204,9 +204,7 @@
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         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)),
+        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}