merged
authorpopescua
Tue May 28 18:51:29 2013 +0200 (2013-05-28)
changeset 52204a3bad3bb9276
parent 52203 055c392e79cf
parent 52202 d5c80b12a1f2
child 52206 6fa21e5a57c3
merged
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 28 16:56:49 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 28 18:51:29 2013 +0200
     1.3 @@ -544,8 +544,7 @@
     1.4          val min_univ_card =
     1.5            NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
     1.6                           (univ_card nat_card int_card main_j0 [] KK.True)
     1.7 -        val _ = if debug then ()
     1.8 -                else check_arity guiltiest_party min_univ_card min_highest_arity
     1.9 +        val _ = check_arity guiltiest_party min_univ_card min_highest_arity
    1.10  
    1.11          val def_us =
    1.12            def_us |> map (choose_reps_in_nut scope unsound rep_table true)
    1.13 @@ -612,7 +611,7 @@
    1.14            fold Integer.max (map (fst o fst) (maps fst bounds)) 0
    1.15          val formula = fold_rev s_and axioms formula
    1.16          val _ = if bits = 0 then () else check_bits bits formula
    1.17 -        val _ = if debug orelse formula = KK.False then ()
    1.18 +        val _ = if formula = KK.False then ()
    1.19                  else check_arity "" univ_card highest_arity
    1.20        in
    1.21          SOME ({comment = comment, settings = settings, univ_card = univ_card,
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue May 28 16:56:49 2013 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue May 28 18:51:29 2013 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4                        else
     2.5                          " of Kodkod relation associated with " ^
     2.6                          quote (original_name guilty_party)) ^
     2.7 -                     " too large for universe of cardinality " ^
     2.8 +                     " too large for a universe of size " ^
     2.9                       string_of_int univ_card)
    2.10    else
    2.11      ()