1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 22:28:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 14 22:29:50 2010 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4     ("theory_relevant", "smart"),
     1.5     ("defs_relevant", "false"),
     1.6     ("isar_proof", "false"),
     1.7 -   ("shrink_factor", "1"),
     1.8 +   ("isar_shrink_factor", "1"),
     1.9     ("minimize_timeout", "5 s")]
    1.10  
    1.11  val alias_params =
    1.12 @@ -116,7 +116,7 @@
    1.13  
    1.14  val params_for_minimize =
    1.15    ["debug", "verbose", "overlord", "full_types", "explicit_apply",
    1.16 -   "isar_proof", "shrink_factor", "minimize_timeout"]
    1.17 +   "isar_proof", "isar_shrink_factor", "minimize_timeout"]
    1.18  
    1.19  val property_dependent_params = ["atps", "full_types", "timeout"]
    1.20  
    1.21 @@ -199,7 +199,7 @@
    1.22      val theory_relevant = lookup_bool_option "theory_relevant"
    1.23      val defs_relevant = lookup_bool "defs_relevant"
    1.24      val isar_proof = lookup_bool "isar_proof"
    1.25 -    val shrink_factor = Int.max (1, lookup_int "shrink_factor")
    1.26 +    val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.27      val timeout = lookup_time "timeout"
    1.28      val minimize_timeout = lookup_time "minimize_timeout"
    1.29    in
    1.30 @@ -208,8 +208,8 @@
    1.31       respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    1.32       relevance_convergence = relevance_convergence,
    1.33       theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    1.34 -     isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
    1.35 -     minimize_timeout = minimize_timeout}
    1.36 +     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    1.37 +     timeout = timeout, minimize_timeout = minimize_timeout}
    1.38    end
    1.39  
    1.40  fun get_params thy = extract_params thy (default_raw_params thy)