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