anchor.diff:          let meta, gl, just = ttac (ASSUME wa) (asl, w)
           meta, (asl, wa) :: gl, fun i l -> PROVE_HYP (hd l) (just i (tl l))
   
  -let SUBGOAL_TAC s tm prfs = 
  +let SUBGOAL_TAC s tm prfs =
       match prfs with
  -    | p :: ps -> 
  -        warn (ps.Length > 0) "SUBGOAL_TAC: additional subproofs ignored"
  -        THENL (SUBGOAL_THEN tm (LABEL_TAC s)) [p; ALL_TAC]
  -    | [] -> failwith "SUBGOAL_TAC: no subproof given"
  +    | p::ps ->
  +        warn (ps.Length <> 0) "SUBGOAL_TAC: additional subproofs ignored"
  +        SUBGOAL_THEN tm (LABEL_TAC s) |> THENL <| [p; ALL_TAC]
  +    |  [] -> failwith "SUBGOAL_TAC: no subproof given"
   
   let (FREEZE_THEN : thm_tactical) = 
       fun ttac th (asl, w) -> 
  
positive.code: (* Theorem continuations.                                                    *)
  (* ------------------------------------------------------------------------- *)
  
  let (CONJUNCTS_THEN2 : thm_tactic -> thm_tactic -> thm_tactic) = 
      fun ttac1 ttac2 cth -> 
          let c1, c2 = dest_conj(concl cth)
          fun gl -> 
              let ti, gls, jfn = (THEN (ttac1(ASSUME c1)) (ttac2(ASSUME c2))) gl
              let jfn' i ths = 
                  let th1, th2 = CONJ_PAIR(INSTANTIATE_ALL i cth)
                  PROVE_HYP th1 (PROVE_HYP th2 (jfn i ths))
              ti, gls, jfn'
  
  let (CONJUNCTS_THEN : thm_tactical) = W CONJUNCTS_THEN2
  
  let (DISJ_CASES_THEN2 : thm_tactic -> thm_tactic -> thm_tactic) = 
      fun ttac1 ttac2 cth -> 
          THENL (DISJ_CASES_TAC cth) [POP_ASSUM ttac1
                                      POP_ASSUM ttac2]
  
  let (DISJ_CASES_THEN : thm_tactical) = W DISJ_CASES_THEN2
  let (DISCH_THEN : thm_tactic -> tactic) = 
      fun ttac -> THEN DISCH_TAC (POP_ASSUM ttac)
  let (X_CHOOSE_THEN : term -> thm_tactical) = 
      fun x ttac th -> THEN (X_CHOOSE_TAC x th) (POP_ASSUM ttac)
  let (CHOOSE_THEN : thm_tactical) = 
      fun ttac th -> THEN (CHOOSE_TAC th) (POP_ASSUM ttac)
  
  (* ------------------------------------------------------------------------- *)
  (* Various derived tactics and theorem continuations.                        *)
  
negative.code:                ASSUME_TAC gth])
  
  let STRUCT_CASES_THEN ttac = REPEAT_TCL STRIP_THM_THEN ttac
  
  let STRUCT_CASES_TAC = 
      STRUCT_CASES_THEN (fun th -> SUBST1_TAC th |> ORELSE <| ASSUME_TAC th);;
  
  let STRIP_GOAL_THEN ttac = 
      FIRST [GEN_TAC
  