# HG changeset patch # User wenzelm # Date 1281542582 -7200 # Node ID 630f379f26605d883ce94ab355ddd9a7558e7831 # Parent c677c2c1d333addf6d76a394ca5bed304eb78bd9 misc tuning and simplification; diff -r c677c2c1d333 -r 630f379f2660 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Aug 11 17:50:29 2010 +0200 +++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 18:03:02 2010 +0200 @@ -28,24 +28,13 @@ (* matching types/consts *) fun matches_subtype thy typat = - let - val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty); - - fun fs [] = false - | fs (t :: ts) = f t orelse fs ts + Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat)); - and f (t as Type (_, ars)) = p t orelse fs ars - | f t = p t; - in f end; - -fun check_const p (nm, (ty, _)) = - if p (nm, ty) - then SOME (Term.size_of_typ ty) - else NONE; +fun check_const pred (nm, (ty, _)) = + if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE; fun opt_not f (c as (_, (ty, _))) = - if is_some (f c) - then NONE else SOME (Term.size_of_typ ty); + if is_some (f c) then NONE else SOME (Term.size_of_typ ty); fun filter_const _ NONE = NONE | filter_const f (SOME (c, r)) = @@ -128,18 +117,15 @@ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; in - Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) - :: Pretty.str "" - :: (Pretty.str o implode) - (if null matches - then ["nothing found", end_msg] - else ["found ", (string_of_int o length) matches, - " constants", end_msg, ":"]) - :: Pretty.str "" - :: map (pretty_const ctxt) matches - |> Pretty.chunks - |> Pretty.writeln - end; + Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: + Pretty.str "" :: + Pretty.str + (if null matches + then "nothing found" ^ end_msg + else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") :: + Pretty.str "" :: + map (pretty_const ctxt) matches + end |> Pretty.chunks |> Pretty.writeln; (* command syntax *) diff -r c677c2c1d333 -r 630f379f2660 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:50:29 2010 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 18:03:02 2010 +0200 @@ -433,23 +433,22 @@ val tally_msg = (case foundo of - NONE => "displaying " ^ string_of_int returned ^ " theorems" + NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" | SOME found => - "found " ^ string_of_int found ^ " theorems" ^ + "found " ^ string_of_int found ^ " theorem(s)" ^ (if returned < found then " (" ^ string_of_int returned ^ " displayed)" else "")); val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; in - Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) - :: Pretty.str "" :: - (if null thms then [Pretty.str ("nothing found" ^ end_msg)] - else - [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ + Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: + Pretty.str "" :: + (if null thms then [Pretty.str ("nothing found" ^ end_msg)] + else + [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ map (pretty_thm ctxt) thms) - |> Pretty.chunks |> Pretty.writeln - end; + end |> Pretty.chunks |> Pretty.writeln;