# HG changeset patch
# User wenzelm
# Date 1267306882 -3600
# Node ID fc130c5e81ecc7915a25c3170677c17a42cf652a
# Parent  de56579ae22933063e04b8a182aa925b36f8603c
code simplification by inlining;

diff -r de56579ae229 -r fc130c5e81ec src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 21:56:55 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 22:41:22 2010 +0100
@@ -257,7 +257,7 @@
 fun obtain_specification_graph options thy t =
   let
     fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
-    fun has_code_pred_intros (c, T) = is_some (try (Predicate_Compile_Core.intros_of thy) c)
+    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
     fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
     fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
     fun defiants_of specs =
@@ -272,14 +272,22 @@
       |> map Const
       (*
       |> filter is_defining_constname*)
-    fun extend t =
-      let
-        val specs = get_specification options thy t
-          (*|> Predicate_Compile_Set.unfold_set_notation*)
-        (*val _ = print_specification options thy constname specs*)
-      in (specs, defiants_of specs) end;
+    fun extend t gr =
+      if can (Term_Graph.get_node gr) t then gr
+      else
+        let
+          val specs = get_specification options thy t
+            (*|> Predicate_Compile_Set.unfold_set_notation*)
+          (*val _ = print_specification options thy constname specs*)
+          val us = defiants_of specs
+        in
+          gr
+          |> Term_Graph.new_node (t, specs)
+          |> fold extend us
+          |> fold (fn u => Term_Graph.add_edge (t, u)) us
+        end
   in
-    Term_Graph.extend extend t Term_Graph.empty
+    extend t Term_Graph.empty
   end;
 
 
diff -r de56579ae229 -r fc130c5e81ec src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Feb 27 21:56:55 2010 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 27 22:41:22 2010 +0100
@@ -48,7 +48,6 @@
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
-  val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
 end;
 
 functor Graph(Key: KEY): GRAPH =
@@ -279,22 +278,6 @@
   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
 
-(* constructing graphs *)
-
-fun extend explore =
-  let
-    fun ext x G =
-      if can (get_entry G) x then G
-      else
-        let val (info, ys) = explore x in
-          G
-          |> new_node (x, info)
-          |> fold ext ys
-          |> fold (fn y => add_edge (x, y)) ys
-        end
-  in ext end;
-
-
 (*final declarations of this structure!*)
 val fold = fold_graph;