1.1 --- a/src/HOL/Library/More_List.thy	Wed Sep 29 11:55:08 2010 +0200
     1.2 +++ b/src/HOL/Library/More_List.thy	Wed Sep 29 15:28:29 2010 +0200
     1.3 @@ -100,8 +100,6 @@
     1.4    "fold plus xs = plus (listsum (rev xs))"
     1.5    by (induct xs) (simp_all add: add.assoc)
     1.6  
     1.7 -declare listsum_foldl [code del]
     1.8 -
     1.9  lemma (in monoid_add) listsum_conv_fold [code]:
    1.10    "listsum xs = fold (\<lambda>x y. y + x) xs 0"
    1.11    by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)

     2.1 --- a/src/Pure/Isar/code.ML	Wed Sep 29 11:55:08 2010 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 29 15:28:29 2010 +0200
     2.3 @@ -1049,8 +1049,8 @@
     2.4      val c = const_eqn thy thm;
     2.5      fun update_subsume thy (thm, proper) eqns = 
     2.6        let
     2.7 -        val args_of = snd o strip_comb o map_types Type.strip_sorts
     2.8 -          o fst o Logic.dest_equals o Thm.plain_prop_of;
     2.9 +        val args_of = dropwhile is_Var o rev o snd o strip_comb
    2.10 +          o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
    2.11          val args = args_of thm;
    2.12          val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
    2.13          fun matches_args args' = length args <= length args' andalso