diff -r a96883a6d709 -r f26c8408a675 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Mon Sep 18 19:12:49 2006 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 18 19:12:50 2006 +0200
@@ -67,14 +67,9 @@
       end);
 
 fun thm_deps thms =
-  let
-    val _ = writeln "Generating graph ...";
-    val gra = map snd (Symtab.dest (fst
-      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))));
-    val path = File.tmp_path (Path.unpack "theorems.graph");
-    val _ = Present.write_graph gra path;
-    val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");
-  in () end;
+  Present.display_graph
+    (map snd (Symtab.dest (fst
+      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
 
 end;