--- 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 ***)