src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

     val _ =
       print silent (fn () =>
           "Testing " ^ n_facts (map fst facts) ^
           (if verbose then
              case timeout of
-               SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+               SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")"
              | _ => ""
            else
              "") ^ "...")
     val {goal, ...} = Proof.goal state
     val facts = facts |> maps (fn (n, ths) => map (pair n) ths)

                 SOME failure => string_of_failure failure
               | NONE =>
                 "Found proof" ^
                  (if length used_facts = length facts then ""
                   else " with " ^ n_facts used_facts) ^
-                 " (" ^ string_from_time run_time ^ ").");
+                 " (" ^ string_of_time run_time ^ ").");
     result
   end
 
 (* minimalization of facts *)
 

     val reserved = reserved_isar_keyword_table ()
     val chained_ths = #facts (Proof.goal state)
     val css = clasimpset_rule_table_of ctxt
     val facts =
       refs |> maps (map (apsnd single)
-                    o fact_from_ref ctxt reserved chained_ths css)
+                    o fact_of_ref ctxt reserved chained_ths css)
   in
     case subgoal_count state of
       0 => Output.urgent_message "No subgoal!"
     | n => case provers of
              [] => error "No prover is set."