src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

                          (filter_used_facts used_facts seen, result)
     | _ => sublinear_minimize test xs (x :: seen, result)
 
 fun binary_minimize test xs =
   let
-    fun p xs = #outcome (test xs : prover_result) = NONE
+    fun pred xs = #outcome (test xs : prover_result) = NONE
     fun split [] p = p
       | split [h] (l, r) = (h :: l, r)
       | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
     fun min _ _ [] = raise Empty
       | min _ _ [s0] = [s0]

                            n_facts (map fst sup) ^ " and " ^
                            n_facts (map fst xs)))
 *)
           val (l0, r0) = split xs ([], [])
         in
-          if p (sup @ l0) then
+          if pred (sup @ l0) then
             min (depth + 1) sup l0
-          else if p (sup @ r0) then
+          else if pred (sup @ r0) then
             min (depth + 1) sup r0
           else
             let
               val l = min (depth + 1) (sup @ r0) l0
               val r = min (depth + 1) (sup @ l) r0

 (*
         |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
 *)
     val xs =
       case min 0 [] xs of
-        [x] => if p [] then [] else [x]
+        [x] => if pred [] then [] else [x]
       | xs => xs
   in (xs, test xs) end
 
 (* Give the external prover some slack. The ATP gets further slack because the
    Sledgehammer preprocessing time is included in the estimate below but isn't