--- a/src/Pure/raw_simplifier.ML Sat May 09 12:19:24 2015 +0200
+++ b/src/Pure/raw_simplifier.ML Tue May 12 08:48:11 2015 +0200
@@ -630,10 +630,6 @@
val a = the (cong_name (head_of lhs)) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
val (xs, weak) = congs;
- val _ =
- if AList.defined (op =) xs a then
- cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a))
- else ();
val xs' = AList.update (op =) (a, thm) xs;
val weak' = if is_full_cong thm then weak else a :: weak;
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);