# HG changeset patch
# User blanchet
# Date 1284402460 -7200
# Node ID d837998f1e6017c6a75bf246ef124de3254633dc
# Parent  062c10ff848cd31dcadf7c7d63c316318555b422
remove "atoms" from the list of options with default values

diff -r 062c10ff848c -r d837998f1e60 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:21:40 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:27:40 2010 +0200
@@ -71,7 +71,6 @@
    ("show_datatypes", "false"),
    ("show_consts", "false"),
    ("format", "1"),
-   ("atoms", ""),
    ("max_potential", "1"),
    ("max_genuine", "1"),
    ("check_potential", "false"),
@@ -105,7 +104,7 @@
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) negated_params s orelse
-  member (op =) ["max", "show_all", "whack", "eval", "expect"] s orelse
+  member (op =) ["max", "show_all", "whack", "atoms", "eval", "expect"] s orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
           "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",