src/Pure/Tools/find_theorems.ML
changeset 46716 c45a4427db39
parent 46713 e6e1ec6d5c1c
child 46717 b09afce1e54f
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:53:34 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:54:50 2012 +0100
     1.3 @@ -586,8 +586,6 @@
     1.4  
     1.5  fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
     1.6    let
     1.7 -    val start = Timing.start ();
     1.8 -
     1.9      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.10      val (foundo, theorems) = find
    1.11        {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
    1.12 @@ -601,14 +599,12 @@
    1.13              (if returned < found
    1.14               then " (" ^ string_of_int returned ^ " displayed)"
    1.15               else ""));
    1.16 -
    1.17 -    val end_msg = " in " ^ Timing.message (Timing.result start);
    1.18    in
    1.19      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    1.20      Pretty.str "" ::
    1.21 -    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
    1.22 +    (if null theorems then [Pretty.str "nothing found"]
    1.23       else
    1.24 -      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
    1.25 +      [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
    1.26          map (pretty_theorem ctxt) theorems)
    1.27    end |> Pretty.chunks |> Pretty.writeln;
    1.28