--- 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);