1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 15:27:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 16:15:10 2010 +0200
     1.3 @@ -94,9 +94,9 @@
     1.4     ("explicit_apply", "false"),
     1.5     ("respect_no_atp", "true"),
     1.6     ("relevance_threshold", "50"),
     1.7 -   ("convergence", "320"),
     1.8 +   ("relevance_convergence", "320"),
     1.9     ("theory_relevant", "smart"),
    1.10 -   ("follow_defs", "false"),
    1.11 +   ("defs_relevant", "false"),
    1.12     ("isar_proof", "false"),
    1.13     ("shrink_factor", "1"),
    1.14     ("minimize_timeout", "5 s")]
    1.15 @@ -111,7 +111,7 @@
    1.16     ("implicit_apply", "explicit_apply"),
    1.17     ("ignore_no_atp", "respect_no_atp"),
    1.18     ("theory_irrelevant", "theory_relevant"),
    1.19 -   ("dont_follow_defs", "follow_defs"),
    1.20 +   ("defs_irrelevant", "defs_relevant"),
    1.21     ("no_isar_proof", "isar_proof")]
    1.22  
    1.23  val params_for_minimize =
    1.24 @@ -194,9 +194,10 @@
    1.25      val respect_no_atp = lookup_bool "respect_no_atp"
    1.26      val relevance_threshold =
    1.27        0.01 * Real.fromInt (lookup_int "relevance_threshold")
    1.28 -    val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
    1.29 +    val relevance_convergence =
    1.30 +      0.01 * Real.fromInt (lookup_int "relevance_convergence")
    1.31      val theory_relevant = lookup_bool_option "theory_relevant"
    1.32 -    val follow_defs = lookup_bool "follow_defs"
    1.33 +    val defs_relevant = lookup_bool "defs_relevant"
    1.34      val isar_proof = lookup_bool "isar_proof"
    1.35      val shrink_factor = Int.max (1, lookup_int "shrink_factor")
    1.36      val timeout = lookup_time "timeout"
    1.37 @@ -205,9 +206,9 @@
    1.38      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    1.39       full_types = full_types, explicit_apply = explicit_apply,
    1.40       respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    1.41 -     convergence = convergence, theory_relevant = theory_relevant,
    1.42 -     follow_defs = follow_defs, isar_proof = isar_proof,
    1.43 -     shrink_factor = shrink_factor, timeout = timeout,
    1.44 +     relevance_convergence = relevance_convergence,
    1.45 +     theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    1.46 +     isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
    1.47       minimize_timeout = minimize_timeout}
    1.48    end
    1.49