--- a/src/Pure/Isar/named_target.ML Fri May 30 08:23:07 2014 +0200
+++ b/src/Pure/Isar/named_target.ML Fri May 30 08:23:07 2014 +0200
@@ -75,11 +75,11 @@
(* abbrev *)
-fun locale_abbrev locale prmode (b, mx) (global_rhs, _) params =
+fun locale_abbrev locale prmode (b, mx) global_rhs params =
Generic_Target.background_abbrev (b, global_rhs) params
#-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
-fun class_abbrev class prmode (b, mx) (global_rhs, _) params =
+fun class_abbrev class prmode (b, mx) global_rhs params =
Generic_Target.background_abbrev (b, global_rhs) params
#-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs);