1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -235,21 +235,21 @@
     1.4      val blocking = auto orelse debug orelse lookup_bool "blocking"
     1.5      val provers = lookup_string "provers" |> space_explode " "
     1.6                    |> auto ? single o hd
     1.7 -    val (type_sys, must_monomorphize) =
     1.8 +    val type_sys =
     1.9        case (lookup_string "type_sys", lookup_bool "full_types") of
    1.10 -        ("many_typed", _) => (Many_Typed, true)
    1.11 -      | ("tags", full_types) => (Tags full_types, false)
    1.12 -      | ("args", full_types) => (Args full_types, false)
    1.13 -      | ("mangled", full_types) => (Mangled full_types, true)
    1.14 -      | ("none", false) => (No_Types, false)
    1.15 +        ("many_typed", _) => Many_Typed
    1.16 +      | ("mangled", full_types) => Mangled full_types
    1.17 +      | ("args", full_types) => Args full_types
    1.18 +      | ("tags", full_types) => Tags full_types
    1.19 +      | ("none", false) => No_Types
    1.20        | (type_sys, full_types) =>
    1.21          if member (op =) ["none", "smart"] type_sys then
    1.22 -          (if full_types then Tags true else Args false, false)
    1.23 +          if full_types then Tags true else Args false
    1.24          else
    1.25            error ("Unknown type system: " ^ quote type_sys ^ ".")
    1.26      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.27      val max_relevant = lookup_int_option "max_relevant"
    1.28 -    val monomorphize = must_monomorphize orelse lookup_bool "monomorphize"
    1.29 +    val monomorphize = lookup_bool "monomorphize"
    1.30      val monomorphize_limit = lookup_int "monomorphize_limit"
    1.31      val explicit_apply = lookup_bool "explicit_apply"
    1.32      val isar_proof = lookup_bool "isar_proof"