1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -35,9 +35,11 @@
     1.4  val supported_proversN = "supported_provers"
     1.5  val kill_proversN = "kill_provers"
     1.6  val running_proversN = "running_provers"
     1.7 +val unlearnN = "unlearn"
     1.8 +val learnN = "learn"
     1.9 +val relearnN = "relearn"
    1.10  val kill_learnersN = "kill_learners"
    1.11  val running_learnersN = "running_learners"
    1.12 -val unlearnN = "unlearn"
    1.13  val refresh_tptpN = "refresh_tptp"
    1.14  
    1.15  val auto = Unsynchronized.ref false
    1.16 @@ -245,8 +247,7 @@
    1.17                           end)]
    1.18    end
    1.19  
    1.20 -val infinity_time_in_secs = 60 * 60 * 24 * 365
    1.21 -val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
    1.22 +val the_timeout = the_default infinite_timeout
    1.23  
    1.24  fun extract_params mode default_params override_params =
    1.25    let
    1.26 @@ -383,12 +384,16 @@
    1.27        kill_provers ()
    1.28      else if subcommand = running_proversN then
    1.29        running_provers ()
    1.30 +    else if subcommand = unlearnN then
    1.31 +      mash_unlearn ctxt
    1.32 +    else if subcommand = learnN orelse subcommand = relearnN then
    1.33 +      (if subcommand = relearnN then mash_unlearn ctxt else ();
    1.34 +       mash_learn ctxt (get_params Normal ctxt
    1.35 +                                   (("verbose", ["true"]) :: override_params)))
    1.36      else if subcommand = kill_learnersN then
    1.37        kill_learners ()
    1.38      else if subcommand = running_learnersN then
    1.39        running_learners ()
    1.40 -    else if subcommand = unlearnN then
    1.41 -      mash_unlearn ctxt
    1.42      else if subcommand = refresh_tptpN then
    1.43        refresh_systems_on_tptp ()
    1.44      else