proof_body/pthm: removed redundant types field;
authorwenzelm
Sun Nov 16 22:12:44 2008 +0100 (2008-11-16)
changeset 28817c8cc94a470d4
parent 28816 d651b0b15835
child 28818 249e394e5b8e
proof_body/pthm: removed redundant types field;
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 22:12:43 2008 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 22:12:44 2008 +0100
     1.3 @@ -251,7 +251,7 @@
     1.4  local
     1.5  
     1.6  fun add_proof_body (PBody {thms, ...}) =
     1.7 -  thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ()));
     1.8 +  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
     1.9  
    1.10  fun add_thm th =
    1.11    (case Thm.proof_body_of th of 
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Sun Nov 16 22:12:43 2008 +0100
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Nov 16 22:12:44 2008 +0100
     2.3 @@ -16,10 +16,10 @@
     2.4  
     2.5  (* thm_deps *)
     2.6  
     2.7 -fun add_dep ((name, _, _), PBody {thms = thms', ...}) =
     2.8 +fun add_dep (name, _, PBody {thms = thms', ...}) =
     2.9    name <> "" ?
    2.10      Graph.new_node (name, ()) #>
    2.11 -    fold (fn (_, ((name', _, _), _)) => name <> "" ? Graph.add_edge (name', name)) thms';
    2.12 +    fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms';
    2.13  
    2.14  fun thm_deps thms =
    2.15    let
    2.16 @@ -60,7 +60,7 @@
    2.17        |> sort_distinct (string_ord o pairself #1);
    2.18  
    2.19      val tab = Proofterm.fold_body_thms
    2.20 -      (fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    2.21 +      (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    2.22        (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
    2.23      fun is_unused (name, th) =
    2.24        not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));