src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 48397 9fe826095a02
parent 48395 85a7fb65507a
child 48399 4bacc8983b3d
equal deleted inserted replaced
48396:dd82d190c2af 48397:9fe826095a02
   149                             | _ => value)
   149                             | _ => value)
   150     | NONE => (name, value)
   150     | NONE => (name, value)
   151 
   151 
   152 val any_type_enc = type_enc_from_string Strict "erased"
   152 val any_type_enc = type_enc_from_string Strict "erased"
   153 
   153 
   154 (* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted.
   154 (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
   155    For the last three, this is a secret feature. *)
   155    can be omitted. For the last four, this is a secret feature. *)
   156 fun normalize_raw_param ctxt =
   156 fun normalize_raw_param ctxt =
   157   unalias_raw_param
   157   unalias_raw_param
   158   #> (fn (name, value) =>
   158   #> (fn (name, value) =>
   159          if is_known_raw_param name then
   159          if is_known_raw_param name then
   160            (name, value)
   160            (name, value)
   165          else if can (trans_lams_from_string ctxt any_type_enc) name andalso
   165          else if can (trans_lams_from_string ctxt any_type_enc) name andalso
   166                  null value then
   166                  null value then
   167            ("lam_trans", [name])
   167            ("lam_trans", [name])
   168          else if member (op =) fact_filters name then
   168          else if member (op =) fact_filters name then
   169            ("fact_filter", [name])
   169            ("fact_filter", [name])
   170          else
   170          else case Int.fromString name of
   171            error ("Unknown parameter: " ^ quote name ^ "."))
   171            SOME n => ("max_facts", [name])
       
   172          | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
   172 
   173 
   173 
   174 
   174 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
   175 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
   175    read correctly. *)
   176    read correctly. *)
   176 val implode_param = strip_spaces_except_between_idents o space_implode " "
   177 val implode_param = strip_spaces_except_between_idents o space_implode " "