# HG changeset patch
# User blanchet
# Date 1299158715 -3600
# Node ID 79f837c2e33b3f1849bc40d066fa945a57bcfa7f
# Parent  3f9adc372e0a3e2aac57e6ae0d9c40088f2f8b6a
don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on

diff -r 3f9adc372e0a -r 79f837c2e33b src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 14:25:15 2011 +0100
@@ -335,7 +335,7 @@
     val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
     val _ = List.app check_constr_nut need_us
     val (free_names, const_names) =
-      fold add_free_and_const_names (nondef_us @ def_us) ([], [])
+      fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
     val (sel_names, nonsel_names) =
       List.partition (is_sel o nickname_of) const_names
     val sound_finitizes =
@@ -343,7 +343,8 @@
                           | _ => false) finitizes)
     val standard = forall snd stds
 (*
-    val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us)
+    val _ =
+      List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
 *)
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
@@ -531,7 +532,7 @@
 (*
         val _ = List.app (print_g o string_for_nut ctxt)
                          (free_names @ sel_names @ nonsel_names @
-                          nondef_us @ def_us)
+                          nondef_us @ def_us @ need_us)
 *)
         val (free_rels, pool, rel_table) =
           rename_free_vars free_names initial_pool NameTable.empty