src/HOL/Tools/Nitpick/nitpick_isar.ML
changeset 43873 f617a5323d07
parent 43865 58150aa44941
child 47823 94aa7b81bcf6
equal deleted inserted replaced
43872:e437d47f419f 43873:f617a5323d07
   276     val show_consts = debug orelse lookup_bool "show_consts"
   276     val show_consts = debug orelse lookup_bool "show_consts"
   277     val evals = lookup_term_list_option_polymorphic "eval" |> these
   277     val evals = lookup_term_list_option_polymorphic "eval" |> these
   278     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   278     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   279     val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
   279     val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
   280     val max_potential =
   280     val max_potential =
   281       if mode = Auto_Try then Int.max (0, lookup_int "max_potential") else 0
   281       if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
   282     val max_genuine = Int.max (0, lookup_int "max_genuine")
   282     val max_genuine = Int.max (0, lookup_int "max_genuine")
   283     val check_potential = lookup_bool "check_potential"
   283     val check_potential = lookup_bool "check_potential"
   284     val check_genuine = lookup_bool "check_genuine"
   284     val check_genuine = lookup_bool "check_genuine"
   285     val batch_size =
   285     val batch_size =
   286       case lookup_int_option "batch_size" of
   286       case lookup_int_option "batch_size" of