1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4     ("strict", "false"),
     1.5     ("lam_trans", "smart"),
     1.6     ("uncurried_aliases", "smart"),
     1.7 +   ("learn", "true"),
     1.8     ("fact_filter", "smart"),
     1.9     ("max_facts", "smart"),
    1.10     ("fact_thresholds", "0.45 0.85"),
    1.11 @@ -108,6 +109,7 @@
    1.12     ("non_blocking", "blocking"),
    1.13     ("non_strict", "strict"),
    1.14     ("no_uncurried_aliases", "uncurried_aliases"),
    1.15 +   ("dont_learn", "learn"),
    1.16     ("no_isar_proof", "isar_proof"),
    1.17     ("dont_slice", "slice"),
    1.18     ("dont_minimize", "minimize")]
    1.19 @@ -296,6 +298,7 @@
    1.20      val strict = mode = Auto_Try orelse lookup_bool "strict"
    1.21      val lam_trans = lookup_option lookup_string "lam_trans"
    1.22      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    1.23 +    val learn = lookup_bool "learn"
    1.24      val fact_filter = lookup_option lookup_string "fact_filter"
    1.25      val max_facts = lookup_option lookup_int "max_facts"
    1.26      val fact_thresholds = lookup_real_pair "fact_thresholds"
    1.27 @@ -317,7 +320,7 @@
    1.28      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.29       provers = provers, type_enc = type_enc, strict = strict,
    1.30       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    1.31 -     fact_filter = fact_filter, max_facts = max_facts,
    1.32 +     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    1.33       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    1.34       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    1.35       isar_shrink_factor = isar_shrink_factor, slice = slice,
    1.36 @@ -371,7 +374,7 @@
    1.37        run_minimize (get_params Minimize ctxt
    1.38                                 (("provers", [default_minimize_prover]) ::
    1.39                                  override_params))
    1.40 -                   (the_default 1 opt_i) (#add fact_override) state
    1.41 +                   (K ()) (the_default 1 opt_i) (#add fact_override) state
    1.42      else if subcommand = messagesN then
    1.43        messages opt_i
    1.44      else if subcommand = supported_proversN then