# HG changeset patch
# User wenzelm
# Date 1030439180 -7200
# Node ID 4813fdc0ef17f802ab21f89e29772fea89bd75b2
# Parent  49a0ad8f175e2299e5d36167ad766998802215f2
Thm.proof_of;

diff -r 49a0ad8f175e -r 4813fdc0ef17 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:07 2002 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:20 2002 +0200
@@ -147,7 +147,7 @@
              | "thm" :: xs =>
                  let val name = NameSpace.pack xs;
                  in (case assoc (thms, name) of
-                     Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
+                     Some thm => fst (strip_combt (Thm.proof_of thm))
                    | None => (case Symtab.lookup (tab, name) of
                          Some prf => prf
                        | None => error ("Unknown theorem " ^ quote name)))
diff -r 49a0ad8f175e -r 4813fdc0ef17 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:07 2002 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 27 11:06:20 2002 +0200
@@ -70,7 +70,7 @@
   let
     val _ = writeln "Generating graph ...";
     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
-      map (#2 o #der o Thm.rep_thm) thms))));
+      map Thm.proof_of 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) ^ " &");