# HG changeset patch
# User wenzelm
# Date 1329253150 -3600
# Node ID 7e6be8270ddb828e20a1e595c610ca15cb10ef88
# Parent  a687b75f9fa871e58ed36759a289d7653cf35566
more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;

diff -r a687b75f9fa8 -r 7e6be8270ddb src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Tue Feb 14 21:45:32 2012 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Tue Feb 14 21:59:10 2012 +0100
@@ -210,11 +210,11 @@
     val tinsts = filter_out has_type_var insts;
 
     (* Tactic *)
-    fun tac i st =
+    fun tac i st = CSUBGOAL (fn (cgoal, _) =>
       let
-        val (_, _, Bi, _) = Thm.dest_state (st, i);
-        val params = Logic.strip_params Bi;  (*params of subgoal i as string typ pairs*)
-        val params = rev (Term.rename_wrt_term Bi params)
+        val goal = term_of cgoal;
+        val params = Logic.strip_params goal;  (*params of subgoal i as string typ pairs*)
+        val params = rev (Term.rename_wrt_term goal params)
           (*as they are printed: bound variables with*)
           (*the same name are renamed during printing*)
 
@@ -266,12 +266,10 @@
         val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate_normalize
               (map lifttvar envT', map liftpair cenv)
-              (Thm.lift_rule (Thm.cprem_of st i) thm)
+              (Thm.lift_rule cgoal thm)
       in
-        if i > nprems_of st then no_tac st
-        else st |>
-          compose_tac (bires_flag, rule, nprems_of thm) i
-      end
+        compose_tac (bires_flag, rule, nprems_of thm) i
+      end) i st
            handle TERM (msg,_)   => (warning msg; no_tac st)
                 | THM  (msg,_,_) => (warning msg; no_tac st);
   in tac end;