don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
authorblanchet
Thu Mar 03 14:25:15 2011 +0100 (2011-03-03 ago)
changeset 4188879f837c2e33b
parent 41877 3f9adc372e0a
child 41889 58c4e0d75492
don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 14:25:15 2011 +0100
     1.3 @@ -335,7 +335,7 @@
     1.4      val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
     1.5      val _ = List.app check_constr_nut need_us
     1.6      val (free_names, const_names) =
     1.7 -      fold add_free_and_const_names (nondef_us @ def_us) ([], [])
     1.8 +      fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
     1.9      val (sel_names, nonsel_names) =
    1.10        List.partition (is_sel o nickname_of) const_names
    1.11      val sound_finitizes =
    1.12 @@ -343,7 +343,8 @@
    1.13                            | _ => false) finitizes)
    1.14      val standard = forall snd stds
    1.15  (*
    1.16 -    val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us)
    1.17 +    val _ =
    1.18 +      List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
    1.19  *)
    1.20  
    1.21      val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
    1.22 @@ -531,7 +532,7 @@
    1.23  (*
    1.24          val _ = List.app (print_g o string_for_nut ctxt)
    1.25                           (free_names @ sel_names @ nonsel_names @
    1.26 -                          nondef_us @ def_us)
    1.27 +                          nondef_us @ def_us @ need_us)
    1.28  *)
    1.29          val (free_rels, pool, rel_table) =
    1.30            rename_free_vars free_names initial_pool NameTable.empty