1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4      (name, value)
     1.5    else if is_prover_list ctxt name andalso null value then
     1.6      ("provers", [name])
     1.7 -  else if can type_enc_from_string name andalso null value then
     1.8 +  else if can (type_enc_from_string Sound) name andalso null value then
     1.9      ("type_enc", [name])
    1.10    else
    1.11      error ("Unknown parameter: " ^ quote name ^ ".")
    1.12 @@ -269,7 +269,7 @@
    1.13          NONE
    1.14        else case lookup_string "type_enc" of
    1.15          "smart" => NONE
    1.16 -      | s => SOME (type_enc_from_string s)
    1.17 +      | s => (type_enc_from_string Sound s; SOME s)
    1.18      val sound = mode = Auto_Try orelse lookup_bool "sound"
    1.19      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.20      val max_relevant = lookup_option lookup_int "max_relevant"