unbreak "max_potential" logic
authorblanchet
Fri, 27 May 2011 10:30:08 +0200
changeset 43032 f617a5323d07
parent 43031 e437d47f419f
child 43033 c4b9b4be90c4
unbreak "max_potential" logic
src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
@@ -278,7 +278,7 @@
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
     val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
     val max_potential =
-      if mode = Auto_Try then Int.max (0, lookup_int "max_potential") else 0
+      if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
     val max_genuine = Int.max (0, lookup_int "max_genuine")
     val check_potential = lookup_bool "check_potential"
     val check_genuine = lookup_bool "check_genuine"