# HG changeset patch
# User berghofe
# Date 1238675950 -7200
# Node ID 5e20f9c2008618fd6936f97e3d211af89b3dd687
# Parent  bf99ceb7d01537a8a8f860eab600f8a73d335a03
Fixed bug in transformation of congruence rule for ==
(thanks to Andy Schropp for reporting this).

diff -r bf99ceb7d015 -r 5e20f9c20086 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Apr 01 16:55:31 2009 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Thu Apr 02 14:39:10 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/rewrite_hol_proof.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Rewrite rules for HOL proofs
@@ -71,7 +70,7 @@
  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
- \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
+ \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
 
    "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
  \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
@@ -85,7 +84,7 @@
  \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
  \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
  \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
- \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
+ \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
 
    (** rewriting on bool: insert proper congruence rules for logical connectives **)