# HG changeset patch
# User wenzelm
# Date 965238014 -7200
# Node ID 50ec59aff3897dcf520b8451b6b4f6a603ef749f
# Parent  9cd32060bbc866cc66e4af7521a374533973082b
adapted deriv;

diff -r 9cd32060bbc8 -r 50ec59aff389 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Aug 02 19:39:48 2000 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Wed Aug 02 19:40:14 2000 +0200
@@ -66,7 +66,7 @@
   let
     val _ = writeln "Generating graph ...";
     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
-      map (#der o Thm.rep_thm) thms))));
+      map (#2 o #der o Thm.rep_thm) thms))));
     val path = File.tmp_path (Path.unpack "theorems.graph");
     val _ = Present.write_graph gra path;
     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");