src/Pure/tactic.ML
changeset 11929 a77ad6c86564
parent 11774 3bc4f67d7fe1
child 11961 e5911a25d094
     1.1 --- a/src/Pure/tactic.ML	Thu Oct 25 02:11:49 2001 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Oct 25 02:12:10 2001 +0200
     1.3 @@ -106,6 +106,7 @@
     1.4  signature TACTIC =
     1.5  sig
     1.6    include BASIC_TACTIC
     1.7 +  val innermost_params: int -> thm -> (string * typ) list
     1.8    val untaglist: (int * 'a) list -> 'a list
     1.9    val orderlist: (int * 'a) list -> 'a list
    1.10    val rewrite: bool -> thm list -> cterm -> thm
    1.11 @@ -212,6 +213,11 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(*Determine print names of goal parameters (reversed)*)
    1.16 +fun innermost_params i st =
    1.17 +  let val (_, _, Bi, _) = dest_state (st, i)
    1.18 +  in rename_wrt_term Bi (Logic.strip_params Bi) end;
    1.19 +
    1.20  (*Lift and instantiate a rule wrt the given state and subgoal number *)
    1.21  fun lift_inst_rule (st, i, sinsts, rule) =
    1.22  let val {maxidx,sign,...} = rep_thm st