--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Mar 05 16:09:42 2021 +0100
@@ -13,8 +13,6 @@
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
- val time_mult : real -> Time.time -> Time.time
- val time_min : Time.time * Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
@@ -49,9 +47,6 @@
|> tap (fn _ => clean_up x)
|> Exn.release
-fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
-fun time_min (x, y) = if x < y then x else y
-
fun parse_bool_option option name s =
(case s of
"smart" => if option then NONE else raise Option.Option