1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -55,8 +55,7 @@
     1.4  
     1.5  fun pull x xs = x :: filter_out (curry (op =) x) xs
     1.6  
     1.7 -fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
     1.8 -                         : datatype_spec) = true
     1.9 +fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
    1.10    | is_datatype_acyclic _ = false
    1.11  
    1.12  fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
    1.13 @@ -1499,7 +1498,6 @@
    1.14    maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
    1.15         (index_seq 0 (num_sels_for_constr_type T))
    1.16  fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
    1.17 -  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
    1.18    | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
    1.19    | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
    1.20                             {typ, constrs, ...} =