1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:07:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -78,6 +78,7 @@
     1.4     ("debug", "false"),
     1.5     ("verbose", "false"),
     1.6     ("overlord", "false"),
     1.7 +   ("type_sys", "smart"),
     1.8     ("explicit_apply", "false"),
     1.9     ("relevance_thresholds", "0.45 0.85"),
    1.10     ("max_relevant", "smart"),
    1.11 @@ -98,7 +99,7 @@
    1.12     ("no_isar_proof", "isar_proof")]
    1.13  
    1.14  val params_for_minimize =
    1.15 -  ["debug", "verbose", "overlord", "full_types", "isar_proof",
    1.16 +  ["debug", "verbose", "overlord", "full_types", "type_sys", "isar_proof",
    1.17     "isar_shrink_factor", "timeout"]
    1.18  
    1.19  val property_dependent_params = ["provers", "full_types", "timeout"]
    1.20 @@ -221,6 +222,7 @@
    1.21      val provers = lookup_string "provers" |> space_explode " "
    1.22                    |> auto ? single o hd
    1.23      val full_types = lookup_bool "full_types"
    1.24 +    val type_sys = lookup_string "type_sys"
    1.25      val explicit_apply = lookup_bool "explicit_apply"
    1.26      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.27      val max_relevant = lookup_int_option "max_relevant"
    1.28 @@ -230,7 +232,7 @@
    1.29      val expect = lookup_string "expect"
    1.30    in
    1.31      {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
    1.32 -     provers = provers, full_types = full_types,
    1.33 +     provers = provers, full_types = full_types, type_sys = type_sys,
    1.34       explicit_apply = explicit_apply,
    1.35       relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    1.36       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,