tuned signature;

--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Dec 15 21:16:10 2016 +0100
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Dec 15 22:22:45 2016 +0100
@@ -30,7 +30,7 @@
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn (name, _, _) => insert (op =) name) [body] [];
+      (fn {name, ...} => insert (op =) name) [body] [];
 \<close>
 
 text \<open>

--- a/src/Pure/Tools/thm_deps.ML	Thu Dec 15 21:16:10 2016 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Thu Dec 15 22:22:45 2016 +0100
@@ -20,8 +20,8 @@
     fun make_node name directory =
       Graph_Display.session_node
        {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
-    fun add_dep ("", _, _) = I
-      | add_dep (name, _, PBody {thms = thms', ...}) =
+    fun add_dep {name = "", ...} = I
+      | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
           let
             val prefix = #1 (split_last (Long_Name.explode name));
             val session =
@@ -73,7 +73,7 @@
 
     val used =
       Proofterm.fold_body_thms
-        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
+        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
         (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
         Symtab.empty;
 

--- a/src/Pure/proofterm.ML	Thu Dec 15 21:16:10 2016 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 15 22:22:45 2016 +0100
@@ -40,7 +40,8 @@
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
-  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+  val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+    proof_body list -> 'a -> 'a
   val join_bodies: proof_body list -> unit
   val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
@@ -213,7 +214,7 @@
           let
             val body' = Future.join body;
             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-          in (f (name, prop, body') x', seen') end);
+          in (f {serial = i, name = name, prop = prop, body = body'} x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();