src/Pure/Tools/find_theorems.ML
changeset 43069 88e45168272c
parent 43068 ac769b5edd1d
child 43070 0318781be055
     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;