1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 03 22:33:23 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 03 22:51:32 2010 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4     ("verbose", "false"),
     1.5     ("overlord", "false"),
     1.6     ("explicit_apply", "false"),
     1.7 -   ("relevance_thresholds", "45 85"),
     1.8 +   ("relevance_thresholds", "0.45 0.85"),
     1.9     ("max_relevant", "smart"),
    1.10     ("isar_proof", "false"),
    1.11     ("isar_shrink_factor", "1")]
    1.12 @@ -206,14 +206,14 @@
    1.13                      SOME n => n
    1.14                    | NONE => error ("Parameter " ^ quote name ^
    1.15                                     " must be assigned an integer value.")
    1.16 -    fun lookup_int_pair name =
    1.17 +    fun lookup_real_pair name =
    1.18        case lookup name of
    1.19 -        NONE => (0, 0)
    1.20 -      | SOME s => case s |> space_explode " " |> map Int.fromString of
    1.21 -                    [SOME n1, SOME n2] => (n1, n2)
    1.22 +        NONE => (0.0, 0.0)
    1.23 +      | SOME s => case s |> space_explode " " |> map Real.fromString of
    1.24 +                    [SOME r1, SOME r2] => (r1, r2)
    1.25                    | _ => error ("Parameter " ^ quote name ^
    1.26 -                                "must be assigned a pair of integer values \
    1.27 -                                \(e.g., \"60 95\")")
    1.28 +                                "must be assigned a pair of floating-point \
    1.29 +                                \values (e.g., \"0.6 0.95\")")
    1.30      fun lookup_int_option name =
    1.31        case lookup name of
    1.32          SOME "smart" => NONE
    1.33 @@ -226,9 +226,7 @@
    1.34                    |> auto ? single o hd
    1.35      val full_types = lookup_bool "full_types"
    1.36      val explicit_apply = lookup_bool "explicit_apply"
    1.37 -    val relevance_thresholds =
    1.38 -      lookup_int_pair "relevance_thresholds"
    1.39 -      |> pairself (fn n => 0.01 * Real.fromInt n)
    1.40 +    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.41      val max_relevant = lookup_int_option "max_relevant"
    1.42      val isar_proof = lookup_bool "isar_proof"
    1.43      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")