src/Pure/Tools/find_theorems.ML
changeset 32738 15bb09ca0378
parent 32149 ef59550a55d3
child 32798 4b85b59a9f66
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4    datatype 'term criterion =
     1.5      Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
     1.6      Pattern of 'term
     1.7 -  val tac_limit: int ref
     1.8 -  val limit: int ref
     1.9 +  val tac_limit: int Unsynchronized.ref
    1.10 +  val limit: int Unsynchronized.ref
    1.11    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.12      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    1.13    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.14 @@ -186,7 +186,7 @@
    1.15      end
    1.16    else NONE
    1.17  
    1.18 -val tac_limit = ref 5;
    1.19 +val tac_limit = Unsynchronized.ref 5;
    1.20  
    1.21  fun filter_solves ctxt goal =
    1.22    let
    1.23 @@ -372,7 +372,7 @@
    1.24     (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
    1.25      Facts.dest_static [] (ProofContext.facts_of ctxt));
    1.26  
    1.27 -val limit = ref 40;
    1.28 +val limit = Unsynchronized.ref 40;
    1.29  
    1.30  fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.31    let