--- 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])))));
--- 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) =
--- 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 ****)