# HG changeset patch
# User berghofe
# Date 1225445854 -3600
# Node ID 4f2954d995f00adc1737756beef188082d1a5f10
# Parent  60e51a0457558fcc6e6c32f76df5ac980bc9dd93
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
to eta-contracted proofs.

diff -r 60e51a045755 -r 4f2954d995f0 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 31 10:35:30 2008 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 31 10:37:34 2008 +0100
@@ -23,15 +23,15 @@
 
   ["(equal_elim % x1 % x2 %% \
  \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
- \      (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) ==  \
+ \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
  \  (iffD1 % A % B %%  \
- \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
+ \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
 
    "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
  \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
- \      (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) ==  \
+ \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
  \  (iffD2 % A % B %%  \
- \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
+ \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
 
    "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
  \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \