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 =