src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   val parse_time_option : string -> string -> Time.time option
   val subgoal_count : Proof.state -> int
   val reserved_isar_keyword_table : unit -> unit Symtab.table
   val thms_in_proof : string Symtab.table option -> thm -> string list
   val thms_of_name : Proof.context -> string -> thm list
+  val one_day : Time.time
+  val one_year : Time.time
+  val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
 end;
 
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
 struct

     |> Token.source_proper
     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
     |> Source.exhaust
   end
 
+val one_day = seconds (24.0 * 60.0 * 60.0)
+val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
+
+fun time_limit NONE = I
+  | time_limit (SOME delay) = TimeLimit.timeLimit delay
+
 fun with_vanilla_print_mode f x =
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                            (print_mode_value ())) f x
 
 end;