src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Thu Sep 30 09:45:18 2010 +0200
+++ b/src/Pure/Isar/code.ML	Thu Sep 30 18:37:29 2010 +0200
@@ -1049,7 +1049,7 @@
     val c = const_eqn thy thm;
     fun update_subsume thy (thm, proper) eqns = 
       let
-        val args_of = dropwhile is_Var o rev o snd o strip_comb
+        val args_of = drop_while 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);