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