--- a/src/Pure/Isar/named_target.ML Mon Jun 02 17:34:27 2014 +0200
+++ b/src/Pure/Isar/named_target.ML Mon Jun 02 19:21:40 2014 +0200
@@ -76,11 +76,11 @@
(* abbrev *)
fun locale_abbrev locale prmode (b, mx) global_rhs params =
- Generic_Target.background_abbrev (b, global_rhs) params
+ Generic_Target.background_abbrev (b, global_rhs) (snd params)
#-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
fun class_abbrev class prmode (b, mx) global_rhs params =
- Generic_Target.background_abbrev (b, global_rhs) params
+ Generic_Target.background_abbrev (b, global_rhs) (snd params)
#-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs);
fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =