Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 13 Apr 2008 14:30:23 +0200
changeset 26636 65343a5ac627
parent 26635 80384c1d1690
child 26637 0bfccafc52eb
tuned;
src/HOL/Tools/rewrite_hol_proof.ML file | annotate | diff | comparison | revisions 
--- 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) =
isabelle