diff --git a/src/combin/combinScript.sml b/src/combin/combinScript.sml
index 58079ccbee..c9044083ce 100644
--- a/src/combin/combinScript.sml
+++ b/src/combin/combinScript.sml
@@ -189,6 +189,8 @@ val UPDATE_APPLY = Q.store_thm("UPDATE_APPLY",
    THEN REPEAT STRIP_TAC
    THEN ASM_REWRITE_TAC [])
 
+Theorem UPDATE_APPLY1 = cj 1 UPDATE_APPLY
+
 val APPLY_UPDATE_THM = Q.store_thm("APPLY_UPDATE_THM",
   `!f a b c. (a =+ b) f c = (if a = c then b else f c)`,
   PURE_REWRITE_TAC [UPDATE_def]
diff --git a/src/simp/src/combinSimps.sml b/src/simp/src/combinSimps.sml
index 717471dd45..5074aae15f 100644
--- a/src/simp/src/combinSimps.sml
+++ b/src/simp/src/combinSimps.sml
@@ -7,7 +7,7 @@ val COMBIN_ss = SSFRAG {
       dprocs = [],
       rewrs = map (fn s => (SOME{Thy="combin",Name= s}, DB.fetch "combin" s)) [
         "I_THM","I_o_ID","K_THM","S_THM","o_ASSOC'","o_THM","W_THM","C_THM",
-        "K_o_THM", "UPDATE_EQ", "UPDATE_APPLY_ID_RWT"
+        "K_o_THM", "UPDATE_EQ", "UPDATE_APPLY_ID_RWT", "UPDATE_APPLY1"
       ]
     }