--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 17:53:19 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 19:00:17 2009 +0100
@@ -716,8 +716,8 @@
(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
- | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
- ({typ, constrs, ...} : dtype_spec) =
+ | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
+ | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
o #const) constrs)
@@ -884,12 +884,13 @@
(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> Kodkod.formula list *)
-fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
- let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
- partition_axioms_for_datatype j0 kk rel_table dtype
- end
+fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
+ | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
+ let val j0 = offset_of_type ofs typ in
+ sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
+ partition_axioms_for_datatype j0 kk rel_table dtype
+ end
(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
-> dtype_spec list -> Kodkod.formula list *)