tuned option name;
authorwenzelm
Thu Apr 17 11:31:46 2014 +0200 (2014-04-17)
changeset 566133518ea9f5200
parent 56612 74851ff86180
child 56614 d80f43dab30e
tuned option name;
etc/options
src/Pure/Tools/find_theorems.ML
     1.1 --- a/etc/options	Thu Apr 17 11:29:15 2014 +0200
     1.2 +++ b/etc/options	Thu Apr 17 11:31:46 2014 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  public option find_theorems_limit : int = 40
     1.5    -- "limit of displayed results"
     1.6  
     1.7 -public option find_theorems_tac_limit : int = 5
     1.8 +public option find_theorems_tactic_limit : int = 5
     1.9    -- "limit of tactic search for 'solves' criterion"
    1.10  
    1.11  
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Apr 17 11:29:15 2014 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Apr 17 11:31:46 2014 +0200
     2.3 @@ -206,7 +206,7 @@
     2.4      val goal' = Thm.transfer thy' goal;
     2.5  
     2.6      fun limited_etac thm i =
     2.7 -      Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
     2.8 +      Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o etac thm i;
     2.9      fun try_thm thm =
    2.10        if Thm.no_prems thm then rtac thm 1 goal'
    2.11        else