--- 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}