src/HOL/Tools/Nitpick/nitpick_kodkod.ML
changeset 35185 9b8f351cced6
parent 35179 4b198af5beb5
child 35190 ce653cc27a94
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4      hol_context -> int -> int Typtab.table -> kodkod_constrs
     1.5      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
     1.6    val kodkod_formula_from_nut :
     1.7 -    int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
     1.8 +    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
     1.9  end;
    1.10  
    1.11  structure Nitpick_Kodkod : NITPICK_KODKOD =
    1.12 @@ -954,8 +954,8 @@
    1.13    acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
    1.14    maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
    1.15  
    1.16 -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
    1.17 -fun kodkod_formula_from_nut bits ofs liberal
    1.18 +(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
    1.19 +fun kodkod_formula_from_nut bits ofs
    1.20          (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
    1.21                  kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
    1.22                  kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,