src/HOL/Tools/inductive_realizer.ML
changeset 26626 c6231d64d264
parent 26535 66bca8a4079c
child 26663 020618551468
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -24,8 +24,10 @@
     1.4  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
     1.5  
     1.6  fun prf_of thm =
     1.7 -  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
     1.8 -  in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
     1.9 +  let
    1.10 +    val thy = Thm.theory_of_thm thm;
    1.11 +    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    1.12 +  in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    1.13  
    1.14  fun forall_intr_prf (t, prf) =
    1.15    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)