# HG changeset patch
# User haftmann
# Date 1256133241 -7200
# Node ID 3797ae7ffe3c4aa4395b8ad2d2e342640921f094
# Parent  fe166e8b9f07b39b9973dd0a75e4b84bb5cb67ec
more accurate removal

diff -r fe166e8b9f07 -r 3797ae7ffe3c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Oct 21 12:12:21 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Oct 21 15:54:01 2009 +0200
@@ -591,12 +591,15 @@
 
 (** specification of (co)inductive predicates **)
 
+fun drop_first f [] = []
+  | drop_first f (x :: xs) = if f x then xs else x :: drop_first f xs;
+
 fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
   let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
     val argTs = fold (fn c => fn Ts => Ts @
-      (subtract (op =) Ts (List.drop (binder_types (fastype_of c), length params)))) cs [];
+      (fold (fn T => drop_first (curry (op =) T)) Ts (List.drop (binder_types (fastype_of c), length params)))) cs [];
     val k = log 2 1 (length cs);
     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
     val p :: xs = map Free (Variable.variant_frees ctxt intr_ts