# 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;