# HG changeset patch
# User wenzelm
# Date 1312827709 -7200
# Node ID 656ff92bad48615b2e7d04ee91d9feccfcd98bae
# Parent  5d367ceecf564c9efc0d702deedce6767465d8cb
added Reconstruct.proof_of convenience;

diff -r 5d367ceecf56 -r 656ff92bad48 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Aug 08 19:59:35 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Aug 08 20:21:49 2011 +0200
@@ -20,9 +20,6 @@
     in map (fn ks => i::ks) is @ is end
   else [[]];
 
-fun prf_of thm =
-  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
 fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
 
 fun tname_of (Type (s, _)) = s
@@ -141,7 +138,8 @@
                end
           | _ => AbsP ("H", SOME p, prf)))
             (rec_fns ~~ prems_of thm)
-            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+            (Proofterm.proof_combP
+              (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
@@ -201,9 +199,10 @@
           Proofterm.forall_intr_proof' (Logic.varify_global r)
             (AbsP ("H", SOME (Logic.varify_global p), prf)))
         (prems ~~ rs)
-        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+        (Proofterm.proof_combP
+          (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
     val prf' = Extraction.abs_corr_shyps thy' exhaust []
-      (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
+      (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
     val r' = Logic.varify_global (Abs ("y", T,
       list_abs (map dest_Free rs, list_comb (r,
         map Bound ((length rs - 1 downto 0) @ [length rs])))));
diff -r 5d367ceecf56 -r 656ff92bad48 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Aug 08 19:59:35 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Aug 08 20:21:49 2011 +0200
@@ -22,10 +22,8 @@
   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
 
 fun prf_of thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
-  in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
+  Reconstruct.proof_of thm
+  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]
   | subsets (x::xs) =
diff -r 5d367ceecf56 -r 656ff92bad48 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Aug 08 19:59:35 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 08 20:21:49 2011 +0200
@@ -10,6 +10,7 @@
   val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
+  val proof_of : thm -> Proofterm.proof
   val expand_proof : theory -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
 end;
@@ -323,6 +324,10 @@
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
+fun proof_of thm =
+  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+
+
 
 (**** expand and reconstruct subproofs ****)