diff -r 142f1eb707b4 -r befa4e9f7c90 sum.ML
--- a/sum.ML	Thu Sep 16 14:29:14 1993 +0200
+++ b/sum.ML	Wed Sep 22 15:43:05 1993 +0200
@@ -126,5 +126,9 @@
 by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
 val expand_case = result();
 
-(*FIXME: case's congruence rule only should simplifies the first argument*)
 val sum_ss = pair_ss addsimps [case_Inl, case_Inr];
+
+(*Prevents simplification of f and g: much faster*)
+val case_weak_cong = prove_goal Sum.thy
+  "s=t ==> case(s,f,g) = case(t,f,g)"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);