diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
@@ -55,8 +55,7 @@
 
 fun pull x xs = x :: filter_out (curry (op =) x) xs
 
-fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
-                         : datatype_spec) = true
+fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
   | is_datatype_acyclic _ = false
 
 fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
@@ -1499,7 +1498,6 @@
   maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
        (index_seq 0 (num_sels_for_constr_type T))
 fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
-  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
   | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
   | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
                            {typ, constrs, ...} =