# 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) =