tuned signature -- more abstract type thm_node;

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Dec 15 22:22:45 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Dec 16 14:06:31 2016 +0100
@@ -165,15 +165,17 @@
 
 fun fold_body_thms f =
   let
-    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
+    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
       fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
-            val body' = Future.join body
-            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
+            val name = Proofterm.thm_node_name thm_node
+            val prop = Proofterm.thm_node_prop thm_node
+            val body = Future.join (Proofterm.thm_node_body thm_node)
+            val (x', seen') = app (n + (if name = "" then 0 else 1)) body
               (x, Inttab.update (i, ()) seen)
-        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
+        in (x' |> n = 0 ? f (name, prop, body), seen') end)
   in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
 
 in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 15 22:22:45 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Dec 16 14:06:31 2016 +0100
@@ -84,8 +84,10 @@
    be missing over there; or maybe the two code portions are not doing the same? *)
 fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
   let
-    fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
+    fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
       let
+        val name = Proofterm.thm_node_name thm_node
+        val body = Proofterm.thm_node_body thm_node
         val (anonymous, enter_class) =
           (* The "name = outer_name" case caters for the uncommon case where the proved theorem
              occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)

--- a/src/Pure/Tools/thm_deps.ML	Thu Dec 15 22:22:45 2016 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Fri Dec 16 14:06:31 2016 +0100
@@ -35,7 +35,7 @@
                   | NONE => [])
               | _ => ["global"]);
             val node = make_node name (space_implode "/" (session @ prefix));
-            val deps = filter_out (fn s => s = "") (map (#1 o #2) thms');
+            val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
           in Symtab.update (name, (node, deps)) end;
     val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
     val entries1 =

--- a/src/Pure/proofterm.ML	Thu Dec 15 22:22:45 2016 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 16 14:06:31 2016 +0100
@@ -10,6 +10,7 @@
 sig
   val proofs: int Unsynchronized.ref
 
+  type thm_node
   datatype proof =
      MinProof
    | PBound of int
@@ -25,7 +26,7 @@
    | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) Ord_List.T,
-     thms: (serial * (string * term * proof_body future)) Ord_List.T,
+     thms: (serial * thm_node) Ord_List.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -35,9 +36,12 @@
 sig
   include BASIC_PROOFTERM
 
+  type pthm = serial * thm_node
   type oracle = string * term
-  type pthm = serial * (string * term * proof_body future)
   val proof_of: proof_body -> proof
+  val thm_node_name: thm_node -> string
+  val thm_node_prop: thm_node -> term
+  val thm_node_body: thm_node -> proof_body future
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
@@ -176,16 +180,22 @@
  | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) Ord_List.T,
-   thms: (serial * (string * term * proof_body future)) Ord_List.T,
-   proof: proof};
+   thms: (serial * thm_node) Ord_List.T,
+   proof: proof}
+and thm_node = Thm_Node of string * term * proof_body future;
 
 type oracle = string * term;
-type pthm = serial * (string * term * proof_body future);
+type pthm = serial * thm_node;
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
-fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+fun thm_node_name (Thm_Node (name, _, _)) = name;
+fun thm_node_prop (Thm_Node (_, prop, _)) = prop;
+fun thm_node_body (Thm_Node (_, _, body)) = body;
+
+fun join_thms (thms: pthm list) =
+  ignore (Future.joins (map (fn (_, Thm_Node (_, _, body)) => body) thms));
 
 
 (***** proof atoms *****)
@@ -208,7 +218,7 @@
 fun fold_body_thms f =
   let
     fun app (PBody {thms, ...}) =
-      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, Thm_Node (name, prop, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
@@ -224,7 +234,7 @@
     fun status (PBody {oracles, thms, ...}) x =
       let
         val ((oracle, unfinished, failed), seen) =
-          (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) =>
+          (thms, x) |-> fold (fn (i, Thm_Node (_, _, body)) => fn (st, seen) =>
             if Inttab.defined seen i then (st, seen)
             else
               let val seen' = Inttab.update (i, ()) seen in
@@ -246,7 +256,7 @@
 (* proof body *)
 
 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
-fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
+fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
 
 val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
@@ -254,7 +264,7 @@
 val all_oracles_of =
   let
     fun collect (PBody {oracles, thms, ...}) =
-      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, Thm_Node (_, _, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
@@ -267,7 +277,7 @@
   let
     val (oracles, thms) = fold_proof_atoms false
       (fn Oracle (s, prop, _) => apfst (cons (s, prop))
-        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body)))
+        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, Thm_Node (name, prop, body)))
         | _ => I) [prf] ([], []);
   in
     PBody
@@ -311,7 +321,7 @@
     ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
   triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
-and pthm (a, (b, c, body)) =
+and pthm (a, Thm_Node (b, c, body)) =
   pair int (triple string term proof_body) (a, (b, c, Future.join body));
 
 in
@@ -348,7 +358,7 @@
   in PBody {oracles = a, thms = b, proof = c} end
 and pthm x =
   let val (a, (b, c, d)) = pair int (triple string term proof_body) x
-  in (a, (b, c, Future.value d)) end;
+  in (a, Thm_Node (b, c, Future.value d)) end;
 
 in
 
@@ -1606,7 +1616,7 @@
           else new_prf ()
       | _ => new_prf ());
     val head = PThm (i, ((name, prop1, NONE), body'));
-  in ((i, (name, prop1, body')), head, args, argsP, args1) end;
+  in ((i, Thm_Node (name, prop1, body')), head, args, argsP, args1) end;
 
 fun thm_proof thy name shyps hyps concl promises body =
   let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body

--- a/src/Pure/thm.ML	Thu Dec 15 22:22:45 2016 +0100
+++ b/src/Pure/thm.ML	Fri Dec 16 14:06:31 2016 +0100
@@ -1309,9 +1309,9 @@
     val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
     val ps = map (apsnd (Future.map fulfill_body)) promises;
-    val (pthm as (_, (_, prop', _)), proof) =
-      Proofterm.unconstrain_thm_proof thy shyps prop ps body;
+    val (pthm, proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body;
     val der' = make_deriv [] [] [pthm] proof;
+    val prop' = Proofterm.thm_node_prop (#2 pthm);
   in
     Thm (der',
      {cert = cert,