# HG changeset patch
# User blanchet
# Date 1285923481 -7200
# Node ID c986fc8de255cd8eaede46b07377c3815577349d
# Parent  e26d5344e1b751c53af3b2935a13002b86a98731
tuning

diff -r e26d5344e1b7 -r c986fc8de255 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Oct 01 10:39:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Oct 01 10:58:01 2010 +0200
@@ -49,8 +49,6 @@
 
 structure KK = Kodkod
 
-structure NfaGraph = Typ_Graph
-
 fun pull x xs = x :: filter_out (curry (op =) x) xs
 
 fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
@@ -720,19 +718,16 @@
       kk_union (loop_path_rel_expr kk nfa Ts start_T)
                (knot_path_rel_expr kk nfa Ts start_T T start_T)
 
-fun graph_for_nfa nfa =
-  let
-    fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
-    fun add_nfa [] = I
-      | add_nfa ((_, []) :: nfa) = add_nfa nfa
-      | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
-        add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
-        new_node T' o new_node T
-  in add_nfa nfa NfaGraph.empty end
+fun add_nfa_to_graph [] = I
+  | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
+  | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
+    add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
+    Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
 
 fun strongly_connected_sub_nfas nfa =
-  nfa |> graph_for_nfa |> NfaGraph.strong_conn
-      |> map (fn keys => filter (member (op =) keys o fst) nfa)
+  add_nfa_to_graph nfa Typ_Graph.empty
+  |> Typ_Graph.strong_conn
+  |> map (fn keys => filter (member (op =) keys o fst) nfa)
 
 fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
                                   start_T =