src/Pure/Tools/find_consts.ML
changeset 38335 630f379f2660
parent 38334 c677c2c1d333
child 38336 fd53ae1d4c47
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Aug 11 17:50:29 2010 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Aug 11 18:03:02 2010 +0200
     1.3 @@ -28,24 +28,13 @@
     1.4  (* matching types/consts *)
     1.5  
     1.6  fun matches_subtype thy typat =
     1.7 -  let
     1.8 -    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
     1.9 -
    1.10 -    fun fs [] = false
    1.11 -      | fs (t :: ts) = f t orelse fs ts
    1.12 +  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
    1.13  
    1.14 -    and f (t as Type (_, ars)) = p t orelse fs ars
    1.15 -      | f t = p t;
    1.16 -  in f end;
    1.17 -
    1.18 -fun check_const p (nm, (ty, _)) =
    1.19 -  if p (nm, ty)
    1.20 -  then SOME (Term.size_of_typ ty)
    1.21 -  else NONE;
    1.22 +fun check_const pred (nm, (ty, _)) =
    1.23 +  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
    1.24  
    1.25  fun opt_not f (c as (_, (ty, _))) =
    1.26 -  if is_some (f c)
    1.27 -  then NONE else SOME (Term.size_of_typ ty);
    1.28 +  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
    1.29  
    1.30  fun filter_const _ NONE = NONE
    1.31    | filter_const f (SOME (c, r)) =
    1.32 @@ -128,18 +117,15 @@
    1.33  
    1.34      val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
    1.35    in
    1.36 -    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    1.37 -      :: Pretty.str ""
    1.38 -      :: (Pretty.str o implode)
    1.39 -           (if null matches
    1.40 -            then ["nothing found", end_msg]
    1.41 -            else ["found ", (string_of_int o length) matches,
    1.42 -                  " constants", end_msg, ":"])
    1.43 -      :: Pretty.str ""
    1.44 -      :: map (pretty_const ctxt) matches
    1.45 -    |> Pretty.chunks
    1.46 -    |> Pretty.writeln
    1.47 -  end;
    1.48 +    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    1.49 +    Pretty.str "" ::
    1.50 +    Pretty.str
    1.51 +     (if null matches
    1.52 +      then "nothing found" ^ end_msg
    1.53 +      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
    1.54 +    Pretty.str "" ::
    1.55 +    map (pretty_const ctxt) matches
    1.56 +  end |> Pretty.chunks |> Pretty.writeln;
    1.57  
    1.58  
    1.59  (* command syntax *)