# HG changeset patch
# User haftmann
# Date 1222351552 -7200
# Node ID bd4750bcb4e67c7fafa02337a605f964ffafab89
# Parent  5d79c5d684596f1d85686fcdfdf5dd8ff6c6396d
clarifed redundancy policy

diff -r 5d79c5d68459 -r bd4750bcb4e6 src/Pure/Isar/code.ML
--- 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;