# HG changeset patch
# User wenzelm
# Date 1226781095 -3600
# Node ID 7c2e1bbf3c363a3a7e6c83c703afb4d3c950542f
# Parent  7925199a0226a424174d23ce760672f45e1797aa
retrieve thm deps from proof_body;

diff -r 7925199a0226 -r 7c2e1bbf3c36 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Nov 15 21:31:32 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Nov 15 21:31:35 2008 +0100
@@ -250,23 +250,26 @@
 
 local
 
-fun thm_deps th =
-  (case Thm.proof_of th of
-    PThm (name, prf, _, _) =>
-      if Thm.has_name_hint th andalso Thm.get_name_hint th = name then
-        Proofterm.thms_of_proof' prf
+fun add_proof_body (PBody {thms, ...}) =
+  thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ()));
+
+fun add_thm th =
+  (case Thm.proof_of th of 
+    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
+      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
+      then add_proof_body (Lazy.force body)
       else I
-  | prf => Proofterm.thms_of_proof' prf);
+  | body => add_proof_body body);
+
+in
 
 fun thms_deps ths =
   let
     (* FIXME proper derivation names!? *)
     val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
-    val deps = Symtab.keys (fold thm_deps ths Symtab.empty);
+    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
   in (names, deps) end;
 
-in
-
 fun new_thms_deps thy thy' =
   let
     val prev_facts = PureThy.facts_of thy;
@@ -613,9 +616,7 @@
                 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
                 val thy = Context.theory_of_proof ctx
                 val ths = [PureThy.get_thm thy thmname]
-                val deps = filter_out (fn s => s = "")
-                                      (Symtab.keys (fold Proofterm.thms_of_proof
-                                                         (map Thm.proof_of ths) Symtab.empty))
+                val deps = #2 (thms_deps ths);
             in
                 if null deps then ()
                 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,