eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);

--- a/src/Pure/tactic.ML	Tue Feb 14 21:19:39 2012 +0100
+++ b/src/Pure/tactic.ML	Tue Feb 14 21:31:26 2012 +0100
@@ -59,7 +59,6 @@
 signature TACTIC =
 sig
   include BASIC_TACTIC
-  val innermost_params: int -> thm -> (string * typ) list
   val insert_tagged_brl: 'a * (bool * thm) ->
     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
@@ -177,11 +176,6 @@
     val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
   in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
 
-(*Determine print names of goal parameters (reversed)*)
-fun innermost_params i st =
-  let val (_, _, Bi, _) = Thm.dest_state (st, i)
-  in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
-
 
 (*** Applications of cut_rl ***)