--- a/src/Pure/Isar/code.ML Thu Sep 25 14:37:32 2008 +0200
+++ b/src/Pure/Isar/code.ML Thu Sep 25 16:05:52 2008 +0200
@@ -136,8 +136,9 @@
val args = args_of thm;
fun matches_args args' = length args <= length args' andalso
Pattern.matchess thy (args, curry Library.take (length args) args');
- fun drop (thm', _) = if matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
+ fun drop (thm', linear') = if (linear orelse not linear')
+ andalso matches_args (args_of thm') then
+ (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
else false;
in (thm, linear) :: filter_out drop thms end;