# HG changeset patch
# User wenzelm
# Date 1267304215 -3600
# Node ID de56579ae22933063e04b8a182aa925b36f8603c
# Parent  25a67a60678236471b36e08710889c02b9d1890b
just one copy of structure Term_Graph (in Pure);

diff -r 25a67a606782 -r de56579ae229 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 21:56:05 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 21:56:55 2010 +0100
@@ -314,9 +314,6 @@
 
 (*** DEPENDENCY GRAPHS ***)
 
-structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
-
-
 fun prove_chain thy chain_tac c1 c2 =
   let
     val goal =
@@ -342,11 +339,11 @@
 
 
 fun mk_dgraph D cs =
-  TermGraph.empty
-  |> fold (fn c => TermGraph.new_node (c,())) cs
+  Term_Graph.empty
+  |> fold (fn c => Term_Graph.new_node (c, ())) cs
   |> fold_product (fn c1 => fn c2 =>
      if is_none (get_chain D c1 c2 |> the_default NONE)
-     then TermGraph.add_edge (c1, c2) else I)
+     then Term_Graph.add_edge (c1, c2) else I)
      cs cs
 
 fun ucomp_empty_tac T =
@@ -373,7 +370,7 @@
 fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
   let
     val G = mk_dgraph D cs
-    val sccs = TermGraph.strong_conn G
+    val sccs = Term_Graph.strong_conn G
 
     fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
       | split (SCC::rest) i =
diff -r 25a67a606782 -r de56579ae229 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Feb 27 21:56:05 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Feb 27 21:56:55 2010 +0100
@@ -83,7 +83,7 @@
   else
     let
       fun get_specs ts = map_filter (fn t =>
-        TermGraph.get_node gr t |>
+        Term_Graph.get_node gr t |>
         (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths)))
         ts
       val _ = print_step options ("Preprocessing scc of " ^
@@ -123,12 +123,12 @@
     val _ = print_step options "Fetching definitions from theory..."
     val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
           (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
-          |> (fn gr => TermGraph.subgraph (member (op =) (TermGraph.all_succs gr [t])) gr))
+          |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
     val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   in
     Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
       (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
-        (TermGraph.strong_conn gr) thy))
+        (Term_Graph.strong_conn gr) thy))
   end
 
 fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
diff -r 25a67a606782 -r de56579ae229 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Feb 27 21:56:05 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Feb 27 21:56:55 2010 +0100
@@ -4,9 +4,7 @@
 Auxilary functions for predicate compiler.
 *)
 
-(* FIXME proper signature *)
-
-structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
+(* FIXME proper signature! *)
 
 structure Predicate_Compile_Aux =
 struct
diff -r 25a67a606782 -r de56579ae229 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 21:56:05 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 21:56:55 2010 +0100
@@ -14,9 +14,9 @@
   
   val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
   val obtain_specification_graph :
-    Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T
+    Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
     
-  val present_graph : thm list TermGraph.T -> unit
+  val present_graph : thm list Term_Graph.T -> unit
   val normalize_equation : theory -> thm -> thm
 end;
 
@@ -279,7 +279,7 @@
         (*val _ = print_specification options thy constname specs*)
       in (specs, defiants_of specs) end;
   in
-    TermGraph.extend extend t TermGraph.empty
+    Term_Graph.extend extend t Term_Graph.empty
   end;
 
 
@@ -288,11 +288,11 @@
     fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
     fun string_of_const (Const (c, _)) = c
       | string_of_const _ = error "string_of_const: unexpected term"
-    val constss = TermGraph.strong_conn gr;
+    val constss = Term_Graph.strong_conn gr;
     val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
       Termtab.update (const, consts)) consts) constss;
     fun succs consts = consts
-      |> maps (TermGraph.imm_succs gr)
+      |> maps (Term_Graph.imm_succs gr)
       |> subtract eq_cname consts
       |> map (the o Termtab.lookup mapping)
       |> distinct (eq_list eq_cname);
diff -r 25a67a606782 -r de56579ae229 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Sat Feb 27 21:56:05 2010 +0100
+++ b/src/Pure/term_ord.ML	Sat Feb 27 21:56:55 2010 +0100
@@ -226,3 +226,6 @@
 structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
 open Basic_Term_Ord;
 
+
+structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
+