clarified Thm.proof_body_of vs. Thm.proof_of;

--- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -27,8 +27,7 @@
   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
 
 fun prf_of thm =
-  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
-    (Proofterm.proof_of (Thm.proof_of thm));
+  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
 fun prf_subst_vars inst =
   Proofterm.map_proof_terms (subst_vars ([], inst)) I;

--- a/src/HOL/Tools/inductive_realizer.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -18,7 +18,7 @@
 (* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
 fun name_of_thm thm =
   (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
-      [Proofterm.proof_of (Thm.proof_of thm)] [] of
+      [Thm.proof_of thm] [] of
     [name] => name
   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
 
@@ -27,8 +27,7 @@
 fun prf_of thm =
   let
     val thy = Thm.theory_of_thm thm;
-    val thm' =
-      Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm));
+    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
   in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
 
 fun forall_intr_prf t prf =

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -291,8 +291,8 @@
   | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
-val subst_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of subst)));
-val sym_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of sym)));
+val subst_prf = fst (strip_combt (Thm.proof_of subst));
+val sym_prf = fst (strip_combt (Thm.proof_of sym));
 
 fun make_subst Ts prf xs (_, []) = prf
   | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =

--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -469,7 +469,7 @@
         let
           val (ctxt, (_, thm)) = Proof.get_goal state;
           val thy = ProofContext.theory_of ctxt;
-          val prf = Proofterm.proof_of (Thm.proof_of thm);
+          val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
         in

--- a/src/Pure/Proof/extraction.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -714,7 +714,7 @@
       let
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
-        val prf = proof_of (Thm.proof_of thm);
+        val prf = Thm.proof_of thm;
         val name = Thm.get_name thm;
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^

--- a/src/Pure/Proof/proof_syntax.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -109,7 +109,7 @@
              | "thm" :: xs =>
                  let val name = NameSpace.implode xs;
                  in (case AList.lookup (op =) thms name of
-                     SOME thm => fst (strip_combt (Proofterm.proof_of (Thm.proof_of thm)))
+                     SOME thm => fst (strip_combt (Thm.proof_of thm))
                    | NONE => error ("Unknown theorem " ^ quote name))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
@@ -227,7 +227,7 @@
   let
     val thy = Thm.theory_of_thm thm;
     val prop = Thm.full_prop_of thm;
-    val prf = Proofterm.proof_of (Thm.proof_of thm);
+    val prf = Thm.proof_of thm;
     val prf' = (case strip_combt (fst (strip_combP prf)) of
         (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf
       | _ => prf)

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -254,7 +254,7 @@
   thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ()));
 
 fun add_thm th =
-  (case Thm.proof_of th of 
+  (case Thm.proof_body_of th of 
     PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
       if Thm.has_name_hint th andalso Thm.get_name_hint th = name
       then add_proof_body (Lazy.force body)

--- a/src/Pure/Thy/thm_deps.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -23,7 +23,7 @@
 
 fun thm_deps thms =
   let
-    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_of thms) Graph.empty;
+    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty;
     fun add_entry (name, (_, (preds, _))) =
       let
         val prefix = #1 (Library.split_last (NameSpace.explode name));
@@ -61,7 +61,7 @@
 
     val tab = Proofterm.fold_body_thms
       (fn ((name, prop, _), _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
-      (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
+      (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));
 

--- a/src/Pure/thm.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/thm.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -148,7 +148,8 @@
   val freezeT: thm -> thm
   val join_futures: theory -> unit
   val future: (unit -> thm) -> cterm -> thm
-  val proof_of: thm -> proof_body
+  val proof_body_of: thm -> proof_body
+  val proof_of: thm -> proof
   val extern_oracles: theory -> xstring list
   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
@@ -394,9 +395,6 @@
 
 (* basic components *)
 
-fun deriv_of (Thm (Deriv der, _)) = der;
-val proof_term_of = Proofterm.proof_of o #body o deriv_of;
-
 val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
@@ -1660,18 +1658,23 @@
 
 (* fulfilled proof *)
 
-fun proof_of thm =
+fun deriv_of (Thm (Deriv der, _)) = der;
+val raw_proof_of = Proofterm.proof_of o #body o deriv_of;
+
+fun proof_body_of thm =
   let
     val {all_promises, promises, body} = deriv_of thm;
     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
-    val ps = map (apsnd (Lazy.value o proof_term_of o Future.join)) promises;
+    val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
   in Pt.fulfill_proof ps body end;
 
+val proof_of = Proofterm.proof_of o proof_body_of;
+
 
 (* closed derivations with official name *)
 
 fun get_name thm =
-  Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm);
+  Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm);
 
 fun put_name name (thm as Thm (der, args)) =
   let
@@ -1680,7 +1683,7 @@
     val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
 
     val ps =
-      map (apsnd (fn future => Lazy.lazy (fn () => proof_term_of (Future.join future)))) promises;
+      map (apsnd (fn future => Lazy.lazy (fn () => raw_proof_of (Future.join future)))) promises;
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
     val der' = make_deriv [] [] [] [pthm] proof;