# HG changeset patch
# User haftmann
# Date 1401396381 -7200
# Node ID 85e55ea7e06da111b1b298b5d1ea6d3b5b9c6a91
# Parent  ae61587eb44ab7f931ea9f49a362a6532d6b33d8
more direct passing of right-hand side

diff -r ae61587eb44a -r 85e55ea7e06d src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu May 29 22:46:20 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 29 22:46:21 2014 +0200
@@ -79,9 +79,9 @@
   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, rhs') params =
+fun class_abbrev class prmode (b, mx) (global_rhs, _) params =
   Generic_Target.background_abbrev (b, global_rhs) params
-  #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) rhs');
+  #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs);
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =
   if is_class then class_abbrev target