# HG changeset patch
# User wenzelm
# Date 869648856 -7200
# Node ID 7a176613e5d5a1f22fd384134e6328c287c5909f
# Parent  258eee1a056e7bb70e71777748a93f3aaa2af567
tuned congs: standard;

diff -r 258eee1a056e -r 7a176613e5d5 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jul 23 11:04:19 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 23 11:07:36 1997 +0200
@@ -108,8 +108,8 @@
 
 (*Add congruence rules for = (instead of ==) *)
 infix 4 addcongs delcongs;
-fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
-fun ss delcongs congs = ss deleqcongs (congs RL [eq_reflection]);
+fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection]));
+fun ss delcongs congs = ss deleqcongs (map standard (congs RL [eq_reflection]));
 
 fun Addcongs congs = (simpset := !simpset addcongs congs);
 fun Delcongs congs = (simpset := !simpset delcongs congs);