# HG changeset patch
# User wenzelm
# Date 1175722180 -7200
# Node ID 043232f8dde2e44f606f8427a2278da08f59a1dd
# Parent  d920d38f1f02a942c480ef8ffc594f13a3b9d811
removed unused dep_graph;

diff -r d920d38f1f02 -r 043232f8dde2 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Apr 04 23:29:39 2007 +0200
+++ b/src/Pure/theory.ML	Wed Apr 04 23:29:40 2007 +0200
@@ -51,7 +51,6 @@
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
-  val dep_graph: theory -> unit Graph.T;
 end
 
 structure Theory: THEORY =
@@ -330,25 +329,6 @@
   NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))])
     handle Symtab.DUPS dups => err_dup_oras dups);
 
-
-
-(** graph of theory parents **)
-
-fun dep_graph thy =
-  let
-    fun add_thy thy gr =
-      let
-        val name = Context.theory_name thy;
-      in if can (Graph.get_node gr) name then (name, gr)
-      else
-        gr
-        |> Graph.new_node (name, ())
-        |> fold_map add_thy (parents_of thy)
-        |-> (fn names => fold (fn name' => Graph.add_edge (name, name')) names)
-        |> pair name
-      end;
-  in snd (add_thy thy Graph.empty) end;
-
 end;
 
 structure BasicTheory: BASIC_THEORY = Theory;