1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Aug 08 19:59:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Aug 08 20:21:49 2011 +0200
     1.3 @@ -20,9 +20,6 @@
     1.4      in map (fn ks => i::ks) is @ is end
     1.5    else [[]];
     1.6  
     1.7 -fun prf_of thm =
     1.8 -  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
     1.9 -
    1.10  fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
    1.11  
    1.12  fun tname_of (Type (s, _)) = s
    1.13 @@ -141,7 +138,8 @@
    1.14                 end
    1.15            | _ => AbsP ("H", SOME p, prf)))
    1.16              (rec_fns ~~ prems_of thm)
    1.17 -            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.18 +            (Proofterm.proof_combP
    1.19 +              (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
    1.20  
    1.21      val r' =
    1.22        if null is then r
    1.23 @@ -201,9 +199,10 @@
    1.24            Proofterm.forall_intr_proof' (Logic.varify_global r)
    1.25              (AbsP ("H", SOME (Logic.varify_global p), prf)))
    1.26          (prems ~~ rs)
    1.27 -        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.28 +        (Proofterm.proof_combP
    1.29 +          (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
    1.30      val prf' = Extraction.abs_corr_shyps thy' exhaust []
    1.31 -      (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
    1.32 +      (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
    1.33      val r' = Logic.varify_global (Abs ("y", T,
    1.34        list_abs (map dest_Free rs, list_comb (r,
    1.35          map Bound ((length rs - 1 downto 0) @ [length rs])))));

     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Aug 08 19:59:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Aug 08 20:21:49 2011 +0200
     2.3 @@ -22,10 +22,8 @@
     2.4    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     2.5  
     2.6  fun prf_of thm =
     2.7 -  let
     2.8 -    val thy = Thm.theory_of_thm thm;
     2.9 -    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    2.10 -  in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    2.11 +  Reconstruct.proof_of thm
    2.12 +  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
    2.13  
    2.14  fun subsets [] = [[]]
    2.15    | subsets (x::xs) =

     3.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Aug 08 19:59:35 2011 +0200
     3.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 08 20:21:49 2011 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
     3.5    val prop_of' : term list -> Proofterm.proof -> term
     3.6    val prop_of : Proofterm.proof -> term
     3.7 +  val proof_of : thm -> Proofterm.proof
     3.8    val expand_proof : theory -> (string * term option) list ->
     3.9      Proofterm.proof -> Proofterm.proof
    3.10  end;
    3.11 @@ -323,6 +324,10 @@
    3.12  val prop_of' = Envir.beta_eta_contract oo prop_of0;
    3.13  val prop_of = prop_of' [];
    3.14  
    3.15 +fun proof_of thm =
    3.16 +  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    3.17 +
    3.18 +
    3.19  
    3.20  (**** expand and reconstruct subproofs ****)
    3.21