# HG changeset patch
# User wenzelm
# Date 1329238187 -3600
# Node ID 7524f3ac737c612bb4a0ce362ad4acb7e9210114
# Parent  68cf3d3550b5d72ab7e0b2e83e81d39cce365c36
eliminated unused subgoals_tac;

diff -r 68cf3d3550b5 -r 7524f3ac737c src/Pure/Isar/rule_insts.ML
--- 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 >>