diff -r da28fd2852ed -r f1838cf9f139 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Dec 04 23:11:29 2019 +0100
+++ b/src/Pure/raw_simplifier.ML	Wed Dec 04 20:25:21 2019 +0000
@@ -336,7 +336,7 @@
       val rules' = Net.merge eq_rrule (rules1, rules2);
       val prems' = Thm.merge_thms (prems1, prems2);
       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
-      val congs' = merge (Thm.eq_thm_prop o apply2 #2) (congs1, congs2);
+      val congs' = AList.merge (op =) (K true) (congs1, congs2);
       val weak' = merge (op =) (weak1, weak2);
       val procs' = Net.merge eq_proc (procs1, procs2);
       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);