removed unused dep_graph;
authorwenzelm
Wed Apr 04 23:29:40 2007 +0200 (2007-04-04)
changeset 22600043232f8dde2
parent 22599 d920d38f1f02
child 22601 948f23d4af29
removed unused dep_graph;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Wed Apr 04 23:29:39 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Apr 04 23:29:40 2007 +0200
     1.3 @@ -51,7 +51,6 @@
     1.4    val add_finals: bool -> string list -> theory -> theory
     1.5    val add_finals_i: bool -> term list -> theory -> theory
     1.6    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
     1.7 -  val dep_graph: theory -> unit Graph.T;
     1.8  end
     1.9  
    1.10  structure Theory: THEORY =
    1.11 @@ -330,25 +329,6 @@
    1.12    NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))])
    1.13      handle Symtab.DUPS dups => err_dup_oras dups);
    1.14  
    1.15 -
    1.16 -
    1.17 -(** graph of theory parents **)
    1.18 -
    1.19 -fun dep_graph thy =
    1.20 -  let
    1.21 -    fun add_thy thy gr =
    1.22 -      let
    1.23 -        val name = Context.theory_name thy;
    1.24 -      in if can (Graph.get_node gr) name then (name, gr)
    1.25 -      else
    1.26 -        gr
    1.27 -        |> Graph.new_node (name, ())
    1.28 -        |> fold_map add_thy (parents_of thy)
    1.29 -        |-> (fn names => fold (fn name' => Graph.add_edge (name, name')) names)
    1.30 -        |> pair name
    1.31 -      end;
    1.32 -  in snd (add_thy thy Graph.empty) end;
    1.33 -
    1.34  end;
    1.35  
    1.36  structure BasicTheory: BASIC_THEORY = Theory;