src/HOL/Tools/Nitpick/nitpick_tests.ML
changeset 34124 c4628a1dcf75
parent 33982 1ae222745c4a
child 34287 16496e04ca46
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Dec 14 16:48:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Thu Dec 17 15:22:11 2009 +0100
     1.3 @@ -300,6 +300,7 @@
     1.4      val peephole_optim = true
     1.5      val nat_card = 4
     1.6      val int_card = 9
     1.7 +    val bits = 8
     1.8      val j0 = 0
     1.9      val constrs = kodkod_constrs peephole_optim nat_card int_card j0
    1.10      val (free_rels, pool, table) =
    1.11 @@ -307,7 +308,7 @@
    1.12                         NameTable.empty
    1.13      val u = Op1 (Not, type_of u, rep_of u, u)
    1.14              |> rename_vars_in_nut pool table
    1.15 -    val formula = kodkod_formula_from_nut Typtab.empty false constrs u
    1.16 +    val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
    1.17      val bounds = map (bound_for_plain_rel ctxt debug) free_rels
    1.18      val univ_card = univ_card nat_card int_card j0 bounds formula
    1.19      val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)