# HG changeset patch
# User wenzelm
# Date 1245244488 -7200
# Node ID d5d830979a54441c22fa0ddef851a0a207371825
# Parent  7652c87c2db5083d774836c79ae2839258dab113
minor tuning according to Isabelle/ML conventions;
slightly less combinators;

diff -r 7652c87c2db5 -r d5d830979a54 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Jun 17 15:00:19 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Jun 17 15:14:48 2009 +0200
@@ -25,10 +25,9 @@
   | Loose of string
   | Name of string;
 
+
 (* matching types/consts *)
 
-fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
-
 fun matches_subtype thy typat =
   let
     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
@@ -51,7 +50,9 @@
 
 fun filter_const _ NONE = NONE
   | filter_const f (SOME (c, r)) =
-      Option.map (pair c o (curry Int.min r)) (f c);
+      (case f c of
+        NONE => NONE
+      | SOME i => SOME (c, Int.min (r, i)));
 
 
 (* pretty results *)
@@ -76,6 +77,7 @@
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;
 
+
 (* find_consts *)
 
 fun find_consts ctxt raw_criteria =
@@ -85,16 +87,17 @@
     val thy = ProofContext.theory_of ctxt;
     val low_ranking = 10000;
 
-    fun not_internal consts (nm, _) = 
+    fun not_internal consts (nm, _) =
       if member (op =) (Consts.the_tags consts nm) Markup.property_internal
       then NONE else SOME low_ranking;
 
     fun make_pattern crit =
       let
         val raw_T = Syntax.parse_typ ctxt crit;
-        val t = Syntax.check_term
-                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
-                  (Term.dummy_pattern raw_T);
+        val t =
+          Syntax.check_term
+            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+            (Term.dummy_pattern raw_T);
       in Term.type_of t end;
 
     fun make_match (Strict arg) =
@@ -102,34 +105,34 @@
             fn (_, (ty, _)) =>
               let
                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
-                val sub_size = Vartab.fold add_tye tye 0;
+                val sub_size =
+                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
               in SOME sub_size end handle MATCH => NONE
           end
-
       | make_match (Loose arg) =
           check_const (matches_subtype thy (make_pattern arg) o snd)
-      
       | make_match (Name arg) = check_const (match_string arg o fst);
 
     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
     val criteria = map make_criterion raw_criteria;
 
     val consts = Sign.consts_of thy;
-    val (_, consts_tab) = (#constants o Consts.dest) consts;
-    fun eval_entry c = fold filter_const (not_internal consts::criteria)
-                                         (SOME (c, low_ranking));
+    val (_, consts_tab) = #constants (Consts.dest consts);
+    fun eval_entry c =
+      fold filter_const (not_internal consts :: criteria)
+        (SOME (c, low_ranking));
 
     val matches =
       Symtab.fold (cons o eval_entry) consts_tab []
       |> map_filter I
       |> sort (rev_order o int_ord o pairself snd)
-      |> map ((apsnd fst) o fst);
+      |> map (apsnd fst o fst);
 
     val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
       :: Pretty.str ""
-      :: (Pretty.str o concat)
+      :: (Pretty.str o implode)
            (if null matches
             then ["nothing found", end_msg]
             else ["found ", (string_of_int o length) matches,
diff -r 7652c87c2db5 -r d5d830979a54 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Jun 17 15:00:19 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Jun 17 15:14:48 2009 +0200
@@ -282,7 +282,7 @@
           in app (opt_add r r', consts', fs) end;
   in app end;
 
- 
+
 in
 
 fun filter_criterion ctxt opt_goal (b, c) =
@@ -417,7 +417,7 @@
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
     val returned = length thms;
-    
+
     val tally_msg =
       (case foundo of
         NONE => "displaying " ^ string_of_int returned ^ " theorems"