src/Pure/Tools/find_theorems.ML
 changeset 52702 c503730efae5 parent 52701 51dfdcd88e84 child 52703 d68fd63bf082
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:00:35 2013 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 18 22:18:20 2013 +0200
1.3 @@ -20,9 +20,6 @@
1.4      criteria: (bool * 'term criterion) list
1.5    }
1.6
1.7 -  val tac_limit: int Unsynchronized.ref
1.8 -  val limit: int Unsynchronized.ref
1.9 -
1.10    val read_criterion: Proof.context -> string criterion -> term criterion
1.11    val query_parser: (bool * string criterion) list parser
1.12
1.13 @@ -314,11 +311,10 @@
1.14      end
1.15    else NONE;
1.16
1.17 -val tac_limit = Unsynchronized.ref 5;
1.18 -
1.19  fun filter_solves ctxt goal =
1.20    let
1.21 -    fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
1.22 +    fun etacn thm i =
1.23 +      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
1.24      fun try_thm thm =
1.25        if Thm.no_prems thm then rtac thm 1 goal
1.26        else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
1.27 @@ -507,8 +503,6 @@
1.28        visible_facts (Proof_Context.facts_of ctxt))
1.29    end;
1.30
1.31 -val limit = Unsynchronized.ref 40;
1.32 -
1.33  fun filter_theorems ctxt theorems query =
1.34    let
1.35      val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
1.36 @@ -524,7 +518,7 @@
1.37            else raw_matches;
1.38
1.39          val len = length matches;
1.40 -        val lim = the_default (! limit) opt_limit;
1.41 +        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
1.42        in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
1.43
1.44      val find =
```