consts
  meta_keep     :: "bool => prop => prop"

defs
  meta_keep_def : "meta_keep b f == f"

val meta_iffD2 = prove_goal ProtoPure.thy
  "[| PROP P==PROP Q; PROP Q |] ==> PROP P"
  (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);

val meta_iffD1 = symmetric_thm RS meta_iffD2;
val meta_iffDs = [meta_iffD1, meta_iffD2] ;

val _ = ListPair.app bind_thm (["meta_keepD", "meta_keepI"],
  [meta_keep_def] RL meta_iffDs) ;
val _ = bind_thm ("meta_keepTD",
  read_instantiate [("b", "True")] meta_keepD) ;
val _ = bind_thm ("meta_keepFD",
  read_instantiate [("b", "False")] meta_keepD) ;
val _ = bind_thm ("meta_keepF_thin", meta_keepFD RS thin_rl) ;

(* meta_fetac : thm -> int -> int -> tactic
  like fatac n but also deletes hypotheses matched *)
fun meta_fetac th n sg st =
  let val fth = thin_rl RS (replicate n meta_keepFD MRS th) : thm ;
    val subgoal = List.nth (prems_of st, sg - 1) : term ;
    (* turn all subgoal hypotheses H into meta_keep ?b H *)
    val nhyps = length (Logic.strip_assums_hyp subgoal) ;
    val ktac = EVERY' (replicate nhyps (dtac meta_keepI)) : int -> tactic ;
    (* then apply ftac fth - see later *)
    (* then apply atac n times,
      which marks the hypotheses to be deleted with meta_keep False *)
    val atacs = EVERY' (replicate n atac) ;
    (* treat other instances of meta_keep ?b as meta_keep True, and erase *)
    val ekttac = REPEAT o dtac meta_keepTD : int -> tactic ;
    (* delete hypotheses which are (meta_keep False ...) *)
    val ekftac = REPEAT o etac meta_keepF_thin : int -> tactic ;
    (* combine all the above *)
    val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW
      (ekttac THEN' ekftac) : int -> tactic ;
  in ctac sg st end ;