src/Pure/raw_simplifier.ML
changeset 60184 7541f29492c3
parent 59690 46b635624feb
child 60324 f83406084507
     1.1 --- a/src/Pure/raw_simplifier.ML	Sat May 09 12:19:24 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Tue May 12 08:48:11 2015 +0200
     1.3 @@ -630,10 +630,6 @@
     1.4        val a = the (cong_name (head_of lhs)) handle Option.Option =>
     1.5          raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
     1.6        val (xs, weak) = congs;
     1.7 -      val _ =
     1.8 -        if AList.defined (op =) xs a then
     1.9 -          cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a))
    1.10 -        else ();
    1.11        val xs' = AList.update (op =) (a, thm) xs;
    1.12        val weak' = if is_full_cong thm then weak else a :: weak;
    1.13      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);