src/HOL/Tools/inductive_set.ML
changeset 36692 54b64d4ad524
parent 35757 c2884bec5463
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4        | infer (t $ u) = infer t #> infer u
     1.5        | infer _ = I;
     1.6      val new_arities = filter_out
     1.7 -      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
     1.8 +      (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1
     1.9          | _ => false) (fold (snd #> infer) intros []);
    1.10      val params' = map (fn x =>
    1.11        (case AList.lookup op = new_arities x of