# HG changeset patch
# User haftmann
# Date 1285829445 -7200
# Node ID 51451d73c3d4cc7f49dfbc599056752ada3e43e7
# Parent  4bd217def154aef23b1d67746aca918348e85dd5
corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity

diff -r 4bd217def154 -r 51451d73c3d4 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Sep 30 08:50:45 2010 +0200
+++ b/src/Pure/Isar/code.ML	Thu Sep 30 08:50:45 2010 +0200
@@ -1053,8 +1053,13 @@
           o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
         val args = args_of thm;
         val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
-        fun matches_args args' = length args <= length args' andalso
-          Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
+        fun matches_args args' =
+          let
+            val k = length args' - length args
+          in if k >= 0
+            then Pattern.matchess thy (args, (map incr_idx o drop k) args')
+            else false
+          end;
         fun drop (thm', proper') = if (proper orelse not proper')
           andalso matches_args (args_of thm') then 
             (warning ("Code generator: dropping subsumed code equation\n" ^
@@ -1066,7 +1071,8 @@
     fun add_eqn' true (Default (eqns, _)) =
           Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
-      | add_eqn' _ (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
+      | add_eqn' true fun_spec = fun_spec
+      | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
       | add_eqn' false _ = Eqns [(thm, proper)];
   in change_fun_spec false c (add_eqn' default) thy end;