# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID f617a5323d07bef002b36ff04f34426d3f937642
# Parent  e437d47f419f6917d0fed9d4d6cf25dee1d0f81d
unbreak "max_potential" logic

diff -r e437d47f419f -r f617a5323d07 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"