src/HOL/Tools/Nitpick/nitpick.ML
changeset 41802 7592a165fa0b
parent 41801 ed77524f3429
child 41803 ef13e3b7cbaf
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 15:45:44 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 16:33:21 2011 +0100
     1.3 @@ -515,10 +515,12 @@
     1.4                           (univ_card nat_card int_card main_j0 [] KK.True)
     1.5          val _ = check_arity guiltiest_party min_univ_card min_highest_arity
     1.6  
     1.7 -        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
     1.8 -                         def_us
     1.9 -        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
    1.10 -                            nondef_us
    1.11 +        val def_us =
    1.12 +          def_us |> map (choose_reps_in_nut scope unsound rep_table true)
    1.13 +        val nondef_us =
    1.14 +          nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
    1.15 +        val needed_us =
    1.16 +          needed_us |> map (choose_reps_in_nut scope unsound rep_table false)
    1.17  (*
    1.18          val _ = List.app (print_g o string_for_nut ctxt)
    1.19                           (free_names @ sel_names @ nonsel_names @
    1.20 @@ -530,8 +532,9 @@
    1.21            rename_free_vars sel_names pool rel_table
    1.22          val (other_rels, pool, rel_table) =
    1.23            rename_free_vars nonsel_names pool rel_table
    1.24 -        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
    1.25 -        val def_us = map (rename_vars_in_nut pool rel_table) def_us
    1.26 +        val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
    1.27 +        val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
    1.28 +        val needed_us = needed_us |> map (rename_vars_in_nut pool rel_table)
    1.29          val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
    1.30          val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
    1.31          val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True