1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 01 15:53:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 01 15:53:38 2011 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4     ("verbose", "false"),
     1.5     ("overlord", "false"),
     1.6     ("blocking", "false"),
     1.7 -   ("type_sys", "smart"),
     1.8 +   ("type_enc", "smart"),
     1.9     ("sound", "false"),
    1.10     ("relevance_thresholds", "0.45 0.85"),
    1.11     ("max_relevant", "smart"),
    1.12 @@ -107,7 +107,7 @@
    1.13     ("no_slicing", "slicing")]
    1.14  
    1.15  val params_for_minimize =
    1.16 -  ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
    1.17 +  ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
    1.18     "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    1.19     "preplay_timeout"]
    1.20  
    1.21 @@ -124,15 +124,15 @@
    1.22      ss as _ :: _ => forall (is_prover_supported ctxt) ss
    1.23    | _ => false
    1.24  
    1.25 -(* "provers =" and "type_sys =" can be left out. The latter is a secret
    1.26 +(* "provers =" and "type_enc =" can be left out. The latter is a secret
    1.27     feature. *)
    1.28  fun check_and_repair_raw_param ctxt (name, value) =
    1.29    if is_known_raw_param name then
    1.30      (name, value)
    1.31    else if is_prover_list ctxt name andalso null value then
    1.32      ("provers", [name])
    1.33 -  else if can type_sys_from_string name andalso null value then
    1.34 -    ("type_sys", [name])
    1.35 +  else if can type_enc_from_string name andalso null value then
    1.36 +    ("type_enc", [name])
    1.37    else
    1.38      error ("Unknown parameter: " ^ quote name ^ ".")
    1.39  
    1.40 @@ -264,12 +264,12 @@
    1.41        lookup_bool "blocking"
    1.42      val provers = lookup_string "provers" |> space_explode " "
    1.43                    |> mode = Auto_Try ? single o hd
    1.44 -    val type_sys =
    1.45 +    val type_enc =
    1.46        if mode = Auto_Try then
    1.47          NONE
    1.48 -      else case lookup_string "type_sys" of
    1.49 +      else case lookup_string "type_enc" of
    1.50          "smart" => NONE
    1.51 -      | s => SOME (type_sys_from_string s)
    1.52 +      | s => SOME (type_enc_from_string s)
    1.53      val sound = mode = Auto_Try orelse lookup_bool "sound"
    1.54      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.55      val max_relevant = lookup_option lookup_int "max_relevant"
    1.56 @@ -288,7 +288,7 @@
    1.57      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.58       provers = provers, relevance_thresholds = relevance_thresholds,
    1.59       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    1.60 -     max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    1.61 +     max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
    1.62       sound = sound, isar_proof = isar_proof,
    1.63       isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.64       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}