# HG changeset patch
# User wenzelm
# Date 869655289 -7200
# Node ID c9c351374651ef77328464274a8946bfb47bb89c
# Parent  c64410e701fbd3af985b5ac813fbf17da30ac9c0
standard congs;

diff -r c64410e701fb -r c9c351374651 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jul 23 11:54:32 1997 +0200
+++ b/src/FOL/simpdata.ML	Wed Jul 23 12:54:49 1997 +0200
@@ -190,9 +190,9 @@
 (*Add congruence rules for = or <-> (instead of ==) *)
 infix 4 addcongs delcongs;
 fun ss addcongs congs =
-        ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
 fun ss delcongs congs =
-        ss deleqcongs (congs RL [eq_reflection,iff_reflection]);
+        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
 
 fun Addcongs congs = (simpset := !simpset addcongs congs);
 fun Delcongs congs = (simpset := !simpset delcongs congs);