tuned;
authorwenzelm
Sun Apr 13 14:30:23 2008 +0200 (2008-04-13 ago)
changeset 2663665343a5ac627
parent 26635 80384c1d1690
child 26637 0bfccafc52eb
tuned;
src/HOL/Tools/rewrite_hol_proof.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Apr 12 17:00:50 2008 +0200
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Apr 13 14:30:23 2008 +0200
     1.3 @@ -291,8 +291,8 @@
     1.4    | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
     1.5    | strip_cong _ _ = NONE;
     1.6  
     1.7 -val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
     1.8 -val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
     1.9 +val subst_prf = fst (strip_combt (Thm.proof_of subst));
    1.10 +val sym_prf = fst (strip_combt (Thm.proof_of sym));
    1.11  
    1.12  fun make_subst Ts prf xs (_, []) = prf
    1.13    | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =