# HG changeset patch
# User wenzelm
# Date 1003968730 -7200
# Node ID a77ad6c86564df70c8ef1b0c5778ef93088ab4ad
# Parent  d0bae2c3abada16dc3599d2a77b538e4625ea491
innermost_params;

diff -r d0bae2c3abad -r a77ad6c86564 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Oct 25 02:11:49 2001 +0200
+++ b/src/Pure/tactic.ML	Thu Oct 25 02:12:10 2001 +0200
@@ -106,6 +106,7 @@
 signature TACTIC =
 sig
   include BASIC_TACTIC
+  val innermost_params: int -> thm -> (string * typ) list
   val untaglist: (int * 'a) list -> 'a list
   val orderlist: (int * 'a) list -> 'a list
   val rewrite: bool -> thm list -> cterm -> thm
@@ -212,6 +213,11 @@
 end;
 
 
+(*Determine print names of goal parameters (reversed)*)
+fun innermost_params i st =
+  let val (_, _, Bi, _) = dest_state (st, i)
+  in rename_wrt_term Bi (Logic.strip_params Bi) end;
+
 (*Lift and instantiate a rule wrt the given state and subgoal number *)
 fun lift_inst_rule (st, i, sinsts, rule) =
 let val {maxidx,sign,...} = rep_thm st