simpdata.ML

 (*Prevents simplification of x and y: much faster*)
 val if_weak_cong = prove_goal HOL.thy
   "b=c ==> if(b,x,y) = if(c,x,y)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
+(*Prevents simplification of t: much faster*)
+val let_weak_cong = prove_goal HOL.thy
+  "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
 end;