retrieve thm deps from proof_body;
authorwenzelm
Sat Nov 15 21:31:35 2008 +0100 (2008-11-15)
changeset 288097c2e1bbf3c36
parent 28808 7925199a0226
child 28810 e915ab11fe52
retrieve thm deps from proof_body;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Nov 15 21:31:32 2008 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Nov 15 21:31:35 2008 +0100
     1.3 @@ -250,23 +250,26 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun thm_deps th =
     1.8 -  (case Thm.proof_of th of
     1.9 -    PThm (name, prf, _, _) =>
    1.10 -      if Thm.has_name_hint th andalso Thm.get_name_hint th = name then
    1.11 -        Proofterm.thms_of_proof' prf
    1.12 +fun add_proof_body (PBody {thms, ...}) =
    1.13 +  thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ()));
    1.14 +
    1.15 +fun add_thm th =
    1.16 +  (case Thm.proof_of th of 
    1.17 +    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
    1.18 +      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
    1.19 +      then add_proof_body (Lazy.force body)
    1.20        else I
    1.21 -  | prf => Proofterm.thms_of_proof' prf);
    1.22 +  | body => add_proof_body body);
    1.23 +
    1.24 +in
    1.25  
    1.26  fun thms_deps ths =
    1.27    let
    1.28      (* FIXME proper derivation names!? *)
    1.29      val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    1.30 -    val deps = Symtab.keys (fold thm_deps ths Symtab.empty);
    1.31 +    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
    1.32    in (names, deps) end;
    1.33  
    1.34 -in
    1.35 -
    1.36  fun new_thms_deps thy thy' =
    1.37    let
    1.38      val prev_facts = PureThy.facts_of thy;
    1.39 @@ -613,9 +616,7 @@
    1.40                  val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
    1.41                  val thy = Context.theory_of_proof ctx
    1.42                  val ths = [PureThy.get_thm thy thmname]
    1.43 -                val deps = filter_out (fn s => s = "")
    1.44 -                                      (Symtab.keys (fold Proofterm.thms_of_proof
    1.45 -                                                         (map Thm.proof_of ths) Symtab.empty))
    1.46 +                val deps = #2 (thms_deps ths);
    1.47              in
    1.48                  if null deps then ()
    1.49                  else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,