src/Pure/tactic.ML
changeset 15006 107e4dfd3b96
parent 14673 3d760a971fde
child 15011 35be762f58f9
     1.1 --- a/src/Pure/tactic.ML	Thu Jun 24 17:54:53 2004 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Jun 25 14:30:55 2004 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  signature BASIC_TACTIC =
     1.5  sig
     1.6    val ares_tac          : thm list -> int -> tactic
     1.7 -  val asm_rewrite_goal_tac: bool*bool*bool ->
     1.8 -    (MetaSimplifier.meta_simpset -> tactic) -> MetaSimplifier.meta_simpset -> int -> tactic
     1.9    val assume_tac        : int -> tactic
    1.10    val atac      : int ->tactic
    1.11    val bimatch_from_nets_tac:
    1.12 @@ -74,8 +72,6 @@
    1.13    val net_resolve_tac   : thm list -> int -> tactic
    1.14    val norm_hhf_rule     : thm -> thm
    1.15    val norm_hhf_tac      : int -> tactic
    1.16 -  val PRIMITIVE         : (thm -> thm) -> tactic
    1.17 -  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
    1.18    val prune_params_tac  : tactic
    1.19    val rename_params_tac : string list -> int -> tactic
    1.20    val rename_tac        : string -> int -> tactic
    1.21 @@ -137,12 +133,6 @@
    1.22  
    1.23  (*** Basic tactics ***)
    1.24  
    1.25 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    1.26 -fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    1.27 -
    1.28 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    1.29 -fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
    1.30 -
    1.31  (*** The following fail if the goal number is out of range:
    1.32       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
    1.33  
    1.34 @@ -499,24 +489,16 @@
    1.35  
    1.36  (*** Meta-Rewriting Tactics ***)
    1.37  
    1.38 -fun result1 tacf mss thm =
    1.39 -  apsome fst (Seq.pull (tacf mss thm));
    1.40 -
    1.41  val simple_prover =
    1.42 -  result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    1.43 +  SINGLE o (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    1.44  
    1.45  val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    1.46  val simplify = MetaSimplifier.simplify_aux simple_prover;
    1.47  val rewrite_rule = simplify true;
    1.48  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.49  
    1.50 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.51 -fun asm_rewrite_goal_tac mode prover_tac mss =
    1.52 -  SELECT_GOAL
    1.53 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (result1 prover_tac) mss 1));
    1.54 -
    1.55  fun rewrite_goal_tac rews =
    1.56 -  asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
    1.57 +  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
    1.58  
    1.59  (*Rewrite throughout proof state. *)
    1.60  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);