author krauss Mon May 30 17:07:48 2011 +0200 (2011-05-30) changeset 43069 88e45168272c parent 43068 ac769b5edd1d child 43070 0318781be055
moved questionable goal modification out of filter_theorems
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
1.3 @@ -431,13 +431,7 @@
1.4
1.5  fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria =
1.6    let
1.7 -    val assms =
1.8 -      Proof_Context.get_fact ctxt (Facts.named "local.assms")
1.9 -        handle ERROR _ => [];
1.10 -    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.11 -    val opt_goal' = Option.map add_prems opt_goal;
1.12 -
1.13 -    val filters = map (filter_criterion ctxt opt_goal') criteria;
1.14 +    val filters = map (filter_criterion ctxt opt_goal) criteria;
1.15
1.16      fun find_all theorems =
1.17        let
1.18 @@ -464,9 +458,17 @@
1.19      (map (apsnd (read_criterion ctxt)) raw_criteria);
1.20
1.21  fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
1.22 -  filter ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
1.23 -     rem_dups raw_criteria
1.24 -  |> apsnd (map (fn Internal f => f));
1.25 +  let
1.26 +    val assms =
1.27 +      Proof_Context.get_fact ctxt (Facts.named "local.assms")
1.28 +        handle ERROR _ => [];
1.29 +    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.30 +    val opt_goal' = Option.map add_prems opt_goal;
1.31 +  in
1.32 +    filter ctxt (map Internal (all_facts_of ctxt)) opt_goal' opt_limit
1.33 +       rem_dups raw_criteria
1.34 +    |> apsnd (map (fn Internal f => f))
1.35 +  end;
1.36
1.37  val find_theorems = gen_find_theorems filter_theorems;
1.38  val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
```