more parallel find_unused_assms;
authorwenzelm
Mon Dec 17 15:05:22 2012 +0100 (2012-12-17)
changeset 505789efc99c990d5
parent 50576 325bf9073c59
child 50579 8ccffe44d193
more parallel find_unused_assms;
tuned messages;
src/HOL/Tools/Quickcheck/find_unused_assms.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Dec 17 14:51:34 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Dec 17 15:05:22 2012 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4              (s, SOME maximals)
     1.5            end)
     1.6    in
     1.7 -    rev (map check all_thms)
     1.8 +    rev (Par_List.map check all_thms)
     1.9    end
    1.10  
    1.11  
    1.12 @@ -86,14 +86,14 @@
    1.13  local
    1.14  
    1.15  fun pretty_indexes is =
    1.16 -  Pretty.block (separate (Pretty.str " and ")
    1.17 -      (map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is))
    1.18 -     @ [Pretty.brk 1])
    1.19 +  Pretty.block
    1.20 +    (flat (separate [Pretty.str " and", Pretty.brk 1]
    1.21 +      (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
    1.22  
    1.23  fun pretty_thm (s, set_of_indexes) =
    1.24    Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
    1.25      Pretty.str "unnecessary assumption(s) " ::
    1.26 -    separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes))
    1.27 +    separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
    1.28  
    1.29  in
    1.30  
    1.31 @@ -106,11 +106,12 @@
    1.32      val with_superfluous_assumptions =
    1.33        map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results
    1.34  
    1.35 -    val msg = "Found " ^ string_of_int (length with_superfluous_assumptions)
    1.36 -      ^ " theorem(s) with (potentially) superfluous assumptions"
    1.37 -    val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
    1.38 -      ^ " in the theory " ^ quote thy_name
    1.39 -      ^ " with a total of " ^ string_of_int total ^ " theorem(s)"
    1.40 +    val msg =
    1.41 +      "Found " ^ string_of_int (length with_superfluous_assumptions) ^
    1.42 +      " theorems with (potentially) superfluous assumptions"
    1.43 +    val end_msg =
    1.44 +      "Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^
    1.45 +      string_of_int total ^ " total) in the theory " ^ quote thy_name
    1.46    in
    1.47      [Pretty.str (msg ^ ":"), Pretty.str ""] @
    1.48      map pretty_thm with_superfluous_assumptions @
    1.49 @@ -121,7 +122,7 @@
    1.50  
    1.51  val _ =
    1.52    Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
    1.53 -    "find theorems with superfluous assumptions"
    1.54 +    "find theorems with (potentially) superfluous assumptions"
    1.55      (Scan.option Parse.name
    1.56        >> (fn opt_thy_name =>
    1.57          Toplevel.no_timing o Toplevel.keep (fn state =>