src/HOL/Tools/Quickcheck/find_unused_assms.ML

     Pretty.str "unnecessary assumption(s) " ::
     separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes))
 
 fun print_unused_assms ctxt opt_thy_name =
   let
-    val start = Timing.start ()
     val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
     val results = find_unused_assms ctxt thy_name
     val total = length results
     val with_assumptions = length (filter (is_some o snd) results)
     val with_superfluous_assumptions = filter_out (fn (_, r) => r = SOME [])

     val msg = "Found " ^ string_of_int (length with_superfluous_assumptions)
       ^ " theorem(s) with (potentially) superfluous assumptions"      
     val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
       ^ " in the theory " ^ quote thy_name
       ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
-      ^ " in " ^ Timing.message (Timing.result start);
   in
     ([Pretty.str (msg ^ ":"), Pretty.str ""] @
         map pretty_thm with_superfluous_assumptions
     @ [Pretty.str "", Pretty.str end_msg])
   end |> Pretty.chunks |> Pretty.writeln;