# HG changeset patch
# User haftmann
# Date 1285824846 -7200
# Node ID 4b615e3ddef732ea3bf26f24cffe7dd3dfbf302a
# Parent  b1640def6d4450957b49146acd48eb53a108c957# Parent  a914307784799976275356395e90749b86aacf56
merged

diff -r b1640def6d44 -r 4b615e3ddef7 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Thu Sep 30 07:34:06 2010 +0200
@@ -100,8 +100,6 @@
   "fold plus xs = plus (listsum (rev xs))"
   by (induct xs) (simp_all add: add.assoc)
 
-declare listsum_foldl [code del]
-
 lemma (in monoid_add) listsum_conv_fold [code]:
   "listsum xs = fold (\<lambda>x y. y + x) xs 0"
   by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
diff -r b1640def6d44 -r 4b615e3ddef7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Sep 29 17:59:20 2010 +0200
+++ b/src/Pure/Isar/code.ML	Thu Sep 30 07:34:06 2010 +0200
@@ -1049,8 +1049,8 @@
     val c = const_eqn thy thm;
     fun update_subsume thy (thm, proper) eqns = 
       let
-        val args_of = snd o strip_comb o map_types Type.strip_sorts
-          o fst o Logic.dest_equals o Thm.plain_prop_of;
+        val args_of = dropwhile is_Var o rev o snd o strip_comb
+          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