diff -r 04f43a28c97a -r 4ea58120ef3d simpdata.ML
--- a/simpdata.ML	Fri Jan 07 14:22:37 1994 +0100
+++ b/simpdata.ML	Fri Jan 07 14:23:13 1994 +0100
@@ -120,4 +120,9 @@
   "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;