anchor.diff:          then failwith "CHANGED_TAC"
           else gstate
   
  -let rec REPLICATE_TAC n tac = 
  +let rec REPLICATE_TAC n tac =
       if n <= 0
       then ALL_TAC
  -    else THEN tac (REPLICATE_TAC (n - 1) tac)
  +    else
  +        tac |> THEN <|
  +        (REPLICATE_TAC (n - 1) tac)
   
   (* ------------------------------------------------------------------------- *)
   (* Combinators for theorem continuations / "theorem tacticals".              *)
  
positive.code:         with
          | Failure _ -> failwith "CONTR_TAC: Failure."
  
  let (MATCH_ACCEPT_TAC : thm_tactic) = 
      let propagate_thm th i l =
          match l with
          | [] -> INSTANTIATE_ALL i th
          | _ -> failwith "CONTR_TAC.propagate_thm: Unhandled case."
      let rawtac th (asl, w) = 
          try 
              let ith = PART_MATCH I th w
              null_meta, [], propagate_thm ith
          with
          | Failure _ -> failwith "ACCEPT_TAC: Failure."
      fun th -> THEN (REPEAT GEN_TAC) (rawtac th)
  
  let (MATCH_MP_TAC : thm_tactic) = 
      fun th -> 
  
negative.code:         with
          | Failure _ -> failwith "MK_COMB_TAC: Failure."
  
  let (AP_TERM_TAC : tactic) =
       let tac = MK_COMB_TAC |> THENL <| [REFL_TAC; ALL_TAC]
       fun gl ->
           try
               tac gl
           with Failure _ -> failwith "AP_TERM_TAC"
  
  let (AP_THM_TAC : tactic) =
      let tac = MK_COMB_TAC |> THENL <| [ALL_TAC; REFL_TAC]
      fun gl -> 
          try 
              tac gl
          with Failure _ -> failwith "AP_THM_TAC"
  
  let (BINOP_TAC : tactic) =
      let tac = MK_COMB_TAC |> THENL <| [AP_TERM_TAC; ALL_TAC] in
      fun gl -> 
          try 
              tac gl
          with Failure _ -> failwith "AP_THM_TAC";;
  
  let (SUBST1_TAC : thm_tactic) = fun th -> CONV_TAC(SUBS_CONV [th])
  
  let SUBST_ALL_TAC rth =
      SUBST1_TAC rth |> THEN <| RULE_ASSUM_TAC (SUBS [rth])
  
  let BETA_TAC = CONV_TAC(REDEPTH_CONV BETA_CONV)
  
  (* ------------------------------------------------------------------------- *)
  