--- a/src/HOL/Tools/inductive.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Oct 21 10:15:31 2009 +0200
@@ -596,7 +596,7 @@
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
val argTs = fold (fn c => fn Ts => Ts @
- (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
+ (subtract (op =) 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