src/Pure/Tools/find_theorems.ML
 changeset 30822 8aac4b974280 parent 30785 15f64e05e703 child 31042 d452117ba564
1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Mar 31 14:10:46 2009 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 31 20:40:25 2009 +0200
1.3 @@ -271,15 +271,17 @@
1.4        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
1.5    in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
1.7 -fun lazy_filter filters = let
1.8 +fun lazy_filter filters =
1.9 +  let
1.10      fun lazy_match thms = Seq.make (fn () => first_match thms)
1.12      and first_match [] = NONE
1.13 -      | first_match (thm::thms) =
1.14 -          case app_filters thm (SOME (0, 0), NONE, filters) of
1.15 +      | first_match (thm :: thms) =
1.16 +          (case app_filters thm (SOME (0, 0), NONE, filters) of
1.17              NONE => first_match thms
1.18 -          | SOME (_, t) => SOME (t, lazy_match thms);
1.19 +          | SOME (_, t) => SOME (t, lazy_match thms));
1.20    in lazy_match end;
1.21 +
1.22  end;
1.25 @@ -304,9 +306,9 @@
1.26      fun rem_c rev_seen [] = rev rev_seen
1.27        | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
1.28        | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
1.29 -        if Thm.eq_thm_prop (t, t')
1.30 -        then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
1.31 -        else rem_c (x :: rev_seen) (y :: xs)
1.32 +          if Thm.eq_thm_prop (t, t')
1.33 +          then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
1.34 +          else rem_c (x :: rev_seen) (y :: xs)
1.35    in rem_c [] xs end;
1.37  in
1.38 @@ -346,9 +348,10 @@
1.40  fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.41    let
1.42 -    val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
1.43 -                handle ERROR _ => [];
1.44 -    val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1));
1.45 +    val assms =
1.46 +      ProofContext.get_fact ctxt (Facts.named "local.assms")
1.47 +        handle ERROR _ => [];
1.48 +    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.49      val opt_goal' = Option.map add_prems opt_goal;
1.51      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.52 @@ -370,7 +373,7 @@
1.53      val find =
1.54        if rem_dups orelse is_none opt_limit
1.55        then find_all
1.56 -      else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
1.57 +      else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
1.59    in find (all_facts_of ctxt) end;
1.61 @@ -388,12 +391,13 @@
1.62      val returned = length thms;
1.64      val tally_msg =
1.65 -      case foundo of
1.66 +      (case foundo of
1.67          NONE => "displaying " ^ string_of_int returned ^ " theorems"
1.68 -      | SOME found => "found " ^ string_of_int found ^ " theorems" ^
1.69 -                      (if returned < found
1.70 -                       then " (" ^ string_of_int returned ^ " displayed)"
1.71 -                       else "");
1.72 +      | SOME found =>
1.73 +          "found " ^ string_of_int found ^ " theorems" ^
1.74 +            (if returned < found
1.75 +             then " (" ^ string_of_int returned ^ " displayed)"
1.76 +             else ""));
1.78      val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
1.79    in
1.80 @@ -411,11 +415,11 @@
1.82  fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
1.83    Toplevel.unknown_theory o Toplevel.keep (fn state =>
1.84 -  let
1.85 -    val proof_state = Toplevel.enter_proof_body state;
1.86 -    val ctxt = Proof.context_of proof_state;
1.87 -    val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
1.88 -  in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
1.89 +    let
1.90 +      val proof_state = Toplevel.enter_proof_body state;
1.91 +      val ctxt = Proof.context_of proof_state;
1.92 +      val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
1.93 +    in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
1.95  local