# HG changeset patch # User wenzelm # Date 1226869964 -3600 # Node ID c8cc94a470d437004175310dd2a399dc28d2d24a # Parent d651b0b1583585968dcb0bf4da6712abd335b449 proof_body/pthm: removed redundant types field; diff -r d651b0b15835 -r c8cc94a470d4 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 22:12:43 2008 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Nov 16 22:12:44 2008 +0100 @@ -251,7 +251,7 @@ local fun add_proof_body (PBody {thms, ...}) = - thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ())); + thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ())); fun add_thm th = (case Thm.proof_body_of th of diff -r d651b0b15835 -r c8cc94a470d4 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sun Nov 16 22:12:43 2008 +0100 +++ b/src/Pure/Thy/thm_deps.ML Sun Nov 16 22:12:44 2008 +0100 @@ -16,10 +16,10 @@ (* thm_deps *) -fun add_dep ((name, _, _), PBody {thms = thms', ...}) = +fun add_dep (name, _, PBody {thms = thms', ...}) = name <> "" ? Graph.new_node (name, ()) #> - fold (fn (_, ((name', _, _), _)) => name <> "" ? Graph.add_edge (name', name)) thms'; + fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms'; fun thm_deps thms = let @@ -60,7 +60,7 @@ |> sort_distinct (string_ord o pairself #1); val tab = Proofterm.fold_body_thms - (fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) + (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; fun is_unused (name, th) = not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));