1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:23 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -79,11 +79,11 @@
     1.4     ("verbose", "false"),
     1.5     ("overlord", "false"),
     1.6     ("blocking", "false"),
     1.7 +   ("type_sys", "smart"),
     1.8     ("relevance_thresholds", "0.45 0.85"),
     1.9     ("max_relevant", "smart"),
    1.10     ("monomorphize", "false"),
    1.11     ("monomorphize_limit", "4"),
    1.12 -   ("type_sys", "smart"),
    1.13     ("explicit_apply", "false"),
    1.14     ("isar_proof", "false"),
    1.15     ("isar_shrink_factor", "1"),
    1.16 @@ -235,22 +235,22 @@
    1.17      val blocking = auto orelse debug orelse lookup_bool "blocking"
    1.18      val provers = lookup_string "provers" |> space_explode " "
    1.19                    |> auto ? single o hd
    1.20 +    val (type_sys, must_monomorphize) =
    1.21 +      case (lookup_string "type_sys", lookup_bool "full_types") of
    1.22 +        ("many_typed", _) => (Many_Typed, true)
    1.23 +      | ("tags", full_types) => (Tags full_types, false)
    1.24 +      | ("args", full_types) => (Args full_types, false)
    1.25 +      | ("mangled", full_types) => (Mangled full_types, true)
    1.26 +      | ("none", false) => (No_Types, false)
    1.27 +      | (type_sys, full_types) =>
    1.28 +        if member (op =) ["none", "smart"] type_sys then
    1.29 +          (if full_types then Tags true else Args false, false)
    1.30 +        else
    1.31 +          error ("Unknown type system: " ^ quote type_sys ^ ".")
    1.32      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.33      val max_relevant = lookup_int_option "max_relevant"
    1.34 -    val monomorphize = lookup_bool "monomorphize"
    1.35 +    val monomorphize = must_monomorphize orelse lookup_bool "monomorphize"
    1.36      val monomorphize_limit = lookup_int "monomorphize_limit"
    1.37 -    val type_sys =
    1.38 -      case (lookup_string "type_sys", lookup_bool "full_types") of
    1.39 -        ("tags", full_types) => Tags full_types
    1.40 -      | ("args", false) => Args
    1.41 -      | ("mangled", false) => if monomorphize then Mangled else Args
    1.42 -      | ("none", false) => No_Types
    1.43 -      | (type_sys, full_types) =>
    1.44 -        if member (op =) ["args", "mangled", "none", "smart"]
    1.45 -                  type_sys then
    1.46 -          if full_types then Tags true else Args
    1.47 -        else
    1.48 -          error ("Unknown type system: " ^ quote type_sys ^ ".")
    1.49      val explicit_apply = lookup_bool "explicit_apply"
    1.50      val isar_proof = lookup_bool "isar_proof"
    1.51      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")