# 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));