# HG changeset patch
# User blanchet
# Date 1280960471 -7200
# Node ID 51a1bfef9de238792a9cc6500831d8fc8ffbf0a2
# Parent  a8cef06e0480b615a72082a5ce10c2245494f9ce
renamed internal function

diff -r a8cef06e0480 -r 51a1bfef9de2 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 23:27:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 00:21:11 2010 +0200
@@ -53,9 +53,9 @@
 
 fun pull x xs = x :: filter_out (curry (op =) x) xs
 
-fun is_datatype_good_and_old ({co = false, standard = true, deep = true, ...}
-                              : datatype_spec) = true
-  | is_datatype_good_and_old _ = false
+fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
+                         : datatype_spec) = true
+  | is_datatype_acyclic _ = false
 
 fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
 
@@ -315,7 +315,7 @@
            else
              [KK.TupleSet [],
               if T1 = T2 andalso epsilon > delta andalso
-                 is_datatype_good_and_old (the (datatype_spec dtypes T1)) then
+                 is_datatype_acyclic (the (datatype_spec dtypes T1)) then
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
                            KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
@@ -897,7 +897,7 @@
   else
     maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
                                         dtypes)
-         (dtypes |> filter is_datatype_good_and_old
+         (dtypes |> filter is_datatype_acyclic
                  |> filter (fn {constrs = [_], ...} => false
                              | {card, constrs, ...} =>
                                card >= min_sym_break_card andalso