src/HOL/Tools/ATP_Manager/atp_minimal.ML

      the int component of the result should then be removed: *)
   val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
     (string * thm list) list -> ((string * thm list) list * int) option * string
 end
 
-structure ATP_Minimal: ATP_MINIMAL =
+structure ATP_Minimal : ATP_MINIMAL =
 struct
 
 (* Linear minimization *)
 
 fun lin_gen_minimize p s =

           string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
     | (Error, msg) =>
         (NONE, "Error in prover: " ^ msg)
     | (Failure, _) =>
         (NONE, "Failure: No proof with the theorems supplied"))
-    handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
+    handle Sledgehammer_HOL_Clause.TRIVIAL =>
         (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
       | ERROR msg => (NONE, "Error: " ^ msg)
   end