src/Pure/tactic.ML
changeset 214 ed6a3e2b1a33
parent 191 fe5d88d4c7e1
child 230 ec8a2b6aa8a7
     1.1 --- a/src/Pure/tactic.ML	Wed Jan 05 19:29:51 1994 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Jan 05 19:33:56 1994 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    in
     1.5    val ares_tac: thm list -> int -> tactic
     1.6    val asm_rewrite_goal_tac:
     1.7 -        (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
     1.8 +        bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
     1.9    val assume_tac: int -> tactic
    1.10    val atac: int ->tactic
    1.11    val bimatch_from_nets_tac: (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    1.12 @@ -373,8 +373,8 @@
    1.13    | Some(thm,_) => Some(thm);
    1.14  
    1.15  (*Rewrite subgoal i only *)
    1.16 -fun asm_rewrite_goal_tac prover_tac mss i =
    1.17 -      PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i);
    1.18 +fun asm_rewrite_goal_tac mode prover_tac mss i =
    1.19 +      PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
    1.20  
    1.21  (*Rewrite throughout proof state. *)
    1.22  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);