# HG changeset patch
# User haftmann
# Date 1162283335 -3600
# Node ID c9e068f994ba28bc9b767adaf30ecaea1a7895e4
# Parent  624ed9c7c4fe81345dd225ede731b7639d82f18c
added Equals_conv

diff -r 624ed9c7c4fe -r c9e068f994ba src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 31 09:28:54 2006 +0100
+++ b/src/HOL/HOL.thy	Tue Oct 31 09:28:55 2006 +0100
@@ -976,6 +976,13 @@
       in Thm.combination (Thm.reflexive ct1) (conv ct2) end
   | _ => raise TERM ("Trueprop_conv", []));
 
+fun Equals_conv conv ct = (case term_of ct of
+    Const ("op =", _) $ _ $ _ =>
+      let
+        val ((ct1, ct2), ct3) = (apfst Thm.dest_comb o Thm.dest_comb) ct;
+      in Thm.combination (Thm.combination (Thm.reflexive ct1) (conv ct2)) (conv ct3) end
+  | _ => conv ct);
+
 fun constrain_op_eq_thms thy thms =
   let
     fun add_eq (Const ("op =", ty)) =