# HG changeset patch
# User wenzelm
# Date 1208089823 -7200
# Node ID 65343a5ac627e36e7a341c892367fd1f2625188c
# Parent  80384c1d16905b453d85c49e04e44d448715238b
tuned;

diff -r 80384c1d1690 -r 65343a5ac627 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Apr 12 17:00:50 2008 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Apr 13 14:30:23 2008 +0200
@@ -291,8 +291,8 @@
   | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
-val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
-val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
+val subst_prf = fst (strip_combt (Thm.proof_of subst));
+val sym_prf = fst (strip_combt (Thm.proof_of sym));
 
 fun make_subst Ts prf xs (_, []) = prf
   | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =