src/Pure/Tools/find_consts.ML

 datatype criterion =
     Strict of string
   | 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);
 

   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)) =
-      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 *)
 
 fun pretty_criterion (b, c) =

      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
       Pretty.str "::", Pretty.brk 1,
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;
 
+
 (* find_consts *)
 
 fun find_consts ctxt raw_criteria =
   let
     val start = start_timing ();
 
     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) =
           let val qty = make_pattern arg; in
             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,
                   " constants", end_msg, ":"])
       :: Pretty.str ""