src/HOL/Tools/inductive_set.ML

--- a/src/HOL/Tools/inductive_set.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -242,7 +242,7 @@
         NONE => thm' RS sym
       | SOME fs' =>
           let
-            val (_, U) = split_last (binder_types T);
+            val U = List.last (binder_types T);
             val Ts = HOLogic.strip_ptupleT fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;