1.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 21:56:05 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 21:56:55 2010 +0100
     1.3 @@ -314,9 +314,6 @@
     1.4  
     1.5  (*** DEPENDENCY GRAPHS ***)
     1.6  
     1.7 -structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
     1.8 -
     1.9 -
    1.10  fun prove_chain thy chain_tac c1 c2 =
    1.11    let
    1.12      val goal =
    1.13 @@ -342,11 +339,11 @@
    1.14  
    1.15  
    1.16  fun mk_dgraph D cs =
    1.17 -  TermGraph.empty
    1.18 -  |> fold (fn c => TermGraph.new_node (c,())) cs
    1.19 +  Term_Graph.empty
    1.20 +  |> fold (fn c => Term_Graph.new_node (c, ())) cs
    1.21    |> fold_product (fn c1 => fn c2 =>
    1.22       if is_none (get_chain D c1 c2 |> the_default NONE)
    1.23 -     then TermGraph.add_edge (c1, c2) else I)
    1.24 +     then Term_Graph.add_edge (c1, c2) else I)
    1.25       cs cs
    1.26  
    1.27  fun ucomp_empty_tac T =
    1.28 @@ -373,7 +370,7 @@
    1.29  fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
    1.30    let
    1.31      val G = mk_dgraph D cs
    1.32 -    val sccs = TermGraph.strong_conn G
    1.33 +    val sccs = Term_Graph.strong_conn G
    1.34  
    1.35      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
    1.36        | split (SCC::rest) i =

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Feb 27 21:56:05 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Feb 27 21:56:55 2010 +0100
     2.3 @@ -83,7 +83,7 @@
     2.4    else
     2.5      let
     2.6        fun get_specs ts = map_filter (fn t =>
     2.7 -        TermGraph.get_node gr t |>
     2.8 +        Term_Graph.get_node gr t |>
     2.9          (fn ths => if null ths then NONE else SOME (fst (dest_Const t), ths)))
    2.10          ts
    2.11        val _ = print_step options ("Preprocessing scc of " ^
    2.12 @@ -123,12 +123,12 @@
    2.13      val _ = print_step options "Fetching definitions from theory..."
    2.14      val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
    2.15            (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
    2.16 -          |> (fn gr => TermGraph.subgraph (member (op =) (TermGraph.all_succs gr [t])) gr))
    2.17 +          |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
    2.18      val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
    2.19    in
    2.20      Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
    2.21        (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
    2.22 -        (TermGraph.strong_conn gr) thy))
    2.23 +        (Term_Graph.strong_conn gr) thy))
    2.24    end
    2.25  
    2.26  fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =

     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Feb 27 21:56:05 2010 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Feb 27 21:56:55 2010 +0100
     3.3 @@ -4,9 +4,7 @@
     3.4  Auxilary functions for predicate compiler.
     3.5  *)
     3.6  
     3.7 -(* FIXME proper signature *)
     3.8 -
     3.9 -structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
    3.10 +(* FIXME proper signature! *)
    3.11  
    3.12  structure Predicate_Compile_Aux =
    3.13  struct

     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 21:56:05 2010 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Feb 27 21:56:55 2010 +0100
     4.3 @@ -14,9 +14,9 @@
     4.4    
     4.5    val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
     4.6    val obtain_specification_graph :
     4.7 -    Predicate_Compile_Aux.options -> theory -> term -> thm list TermGraph.T
     4.8 +    Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
     4.9      
    4.10 -  val present_graph : thm list TermGraph.T -> unit
    4.11 +  val present_graph : thm list Term_Graph.T -> unit
    4.12    val normalize_equation : theory -> thm -> thm
    4.13  end;
    4.14  
    4.15 @@ -279,7 +279,7 @@
    4.16          (*val _ = print_specification options thy constname specs*)
    4.17        in (specs, defiants_of specs) end;
    4.18    in
    4.19 -    TermGraph.extend extend t TermGraph.empty
    4.20 +    Term_Graph.extend extend t Term_Graph.empty
    4.21    end;
    4.22  
    4.23  
    4.24 @@ -288,11 +288,11 @@
    4.25      fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
    4.26      fun string_of_const (Const (c, _)) = c
    4.27        | string_of_const _ = error "string_of_const: unexpected term"
    4.28 -    val constss = TermGraph.strong_conn gr;
    4.29 +    val constss = Term_Graph.strong_conn gr;
    4.30      val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
    4.31        Termtab.update (const, consts)) consts) constss;
    4.32      fun succs consts = consts
    4.33 -      |> maps (TermGraph.imm_succs gr)
    4.34 +      |> maps (Term_Graph.imm_succs gr)
    4.35        |> subtract eq_cname consts
    4.36        |> map (the o Termtab.lookup mapping)
    4.37        |> distinct (eq_list eq_cname);

     5.1 --- a/src/Pure/term_ord.ML	Sat Feb 27 21:56:05 2010 +0100
     5.2 +++ b/src/Pure/term_ord.ML	Sat Feb 27 21:56:55 2010 +0100
     5.3 @@ -226,3 +226,6 @@
     5.4  structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
     5.5  open Basic_Term_Ord;
     5.6  
     5.7 +
     5.8 +structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
     5.9 +