--- a/src/Pure/Isar/rule_insts.ML Tue Feb 14 17:26:35 2012 +0100
+++ b/src/Pure/Isar/rule_insts.ML Tue Feb 14 17:49:47 2012 +0100
@@ -15,7 +15,6 @@
val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
val thin_tac: Proof.context -> string -> int -> tactic
val subgoal_tac: Proof.context -> string -> int -> tactic
- val subgoals_tac: Proof.context -> string list -> int -> tactic
val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
@@ -314,7 +313,6 @@
(*Introduce the given proposition as lemma and subgoal*)
fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
-fun subgoals_tac ctxt As = EVERY' (map (subgoal_tac ctxt) As);
@@ -355,7 +353,8 @@
Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
Method.setup (Binding.name "subgoal_tac")
(Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props)))
+ (fn (quant, props) => fn ctxt =>
+ SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup (Binding.name "thin_tac")
(Args.goal_spec -- Scan.lift Args.name_source >>