src/Pure/tactic.ML

 fun innermost_params i st =
   let val (_, _, Bi, _) = dest_state (st, i)
   in rename_wrt_term Bi (Logic.strip_params Bi) end;
 
 (*params of subgoal i as they are printed*)
-fun params_of_state st i =
-  let val (_, _, Bi, _) = dest_state(st,i)
-      val params = Logic.strip_params Bi
-  in rev(rename_wrt_term Bi params) end;
+fun params_of_state i st = rev (innermost_params i st);
 
 (*read instantiations with respect to subgoal i of proof state st*)
 fun read_insts_in_state (st, i, sinsts, rule) =
   let val thy = Thm.theory_of_thm st
-      and params = params_of_state st i
+      and params = params_of_state i st
       and rts = types_sorts rule and (types,sorts) = types_sorts st
       fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
         | types' ixn = types ixn;
       val used = Drule.add_used rule (Drule.add_used st []);
   in read_insts thy rts (types',sorts) used sinsts end;
 
 (*Lift and instantiate a rule wrt the given state and subgoal number *)
 fun lift_inst_rule' (st, i, sinsts, rule) =
 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
     and {maxidx,...} = rep_thm st
-    and params = params_of_state st i
+    and params = params_of_state i st
     val paramTs = map #2 params
     and inc = maxidx+1
     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
       | liftvar t = raise TERM("Variable expected", [t]);
     fun liftterm t = list_abs_free (params,

 NB: the types in insts must be correctly instantiated already,
     i.e. Tinsts is not applied to insts.
 *)
 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
 let val {maxidx,thy,...} = rep_thm st
-    val paramTs = map #2 (params_of_state st i)
+    val paramTs = map #2 (params_of_state i st)
     and inc = maxidx+1
     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
     (*lift only Var, not term, which must be lifted already*)
     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
     fun liftTpair (((a, i), S), T) =