src/HOL/Tools/inductive.ML

 
         fun mk_elim_prem ((_, _, us, _), ts, params') =
           list_all (params',
             Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
               (frees ~~ us) @ ts, P));
-        val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs);
+        val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
         val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
            map mk_elim_prem (map #1 c_intrs)
       in
         (Skip_Proof.prove ctxt'' [] prems P
           (fn {prems, ...} => EVERY