# HG changeset patch
# User wenzelm
# Date 1007472382 -3600
# Node ID 86d3218a5410b0cac8907d828453f9bdb58fba8e
# Parent  e853343af65dd7290d156e180c479d7e37e874eb
rules_tac: SELECT_GOAL!!;
tuned;

diff -r e853343af65d -r 86d3218a5410 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Dec 04 02:02:36 2001 +0100
+++ b/src/Pure/Isar/method.ML	Tue Dec 04 14:26:22 2001 +0100
@@ -204,11 +204,11 @@
 
 local
 
-fun remdups_tac i thm =
-  let val prems = Logic.strip_assums_hyp (Library.nth_elem (i - 1, Thm.prems_of thm))
-  in REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
-    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) thm
-  end;
+val remdups_tac = SUBGOAL (fn (g, i) =>
+  let val prems = Logic.strip_assums_hyp g in
+    REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
+    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+  end);
 
 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
 
@@ -245,7 +245,8 @@
 
 in
 
-fun rules_tac ctxt opt_lim = DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4;
+fun rules_tac ctxt opt_lim =
+  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4 1);
 
 end;