228 fun innermost_params i st = 
228 fun innermost_params i st = 
229 let val (_, _, Bi, _) = dest_state (st, i) 
229 let val (_, _, Bi, _) = dest_state (st, i) 
230 in rename_wrt_term Bi (Logic.strip_params Bi) end; 
230 in rename_wrt_term Bi (Logic.strip_params Bi) end; 
231 
231 
232 (*params of subgoal i as they are printed*) 
232 (*params of subgoal i as they are printed*) 
233 fun params_of_state st i = 
233 fun params_of_state i st = rev (innermost_params i st); 
234 let val (_, _, Bi, _) = dest_state(st,i) 

235 val params = Logic.strip_params Bi 

236 in rev(rename_wrt_term Bi params) end; 

237 
234 
238 (*read instantiations with respect to subgoal i of proof state st*) 
235 (*read instantiations with respect to subgoal i of proof state st*) 
239 fun read_insts_in_state (st, i, sinsts, rule) = 
236 fun read_insts_in_state (st, i, sinsts, rule) = 
240 let val thy = Thm.theory_of_thm st 
237 let val thy = Thm.theory_of_thm st 
241 and params = params_of_state st i 
238 and params = params_of_state i st 
242 and rts = types_sorts rule and (types,sorts) = types_sorts st 
239 and rts = types_sorts rule and (types,sorts) = types_sorts st 
243 fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1)  sm => sm) 
240 fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1)  sm => sm) 
244  types' ixn = types ixn; 
241  types' ixn = types ixn; 
245 val used = Drule.add_used rule (Drule.add_used st []); 
242 val used = Drule.add_used rule (Drule.add_used st []); 
246 in read_insts thy rts (types',sorts) used sinsts end; 
243 in read_insts thy rts (types',sorts) used sinsts end; 
247 
244 
248 (*Lift and instantiate a rule wrt the given state and subgoal number *) 
245 (*Lift and instantiate a rule wrt the given state and subgoal number *) 
249 fun lift_inst_rule' (st, i, sinsts, rule) = 
246 fun lift_inst_rule' (st, i, sinsts, rule) = 
250 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) 
247 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) 
251 and {maxidx,...} = rep_thm st 
248 and {maxidx,...} = rep_thm st 
252 and params = params_of_state st i 
249 and params = params_of_state i st 
253 val paramTs = map #2 params 
250 val paramTs = map #2 params 
254 and inc = maxidx+1 
251 and inc = maxidx+1 
255 fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
252 fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
256  liftvar t = raise TERM("Variable expected", [t]); 
253  liftvar t = raise TERM("Variable expected", [t]); 
257 fun liftterm t = list_abs_free (params, 
254 fun liftterm t = list_abs_free (params, 
281 NB: the types in insts must be correctly instantiated already, 
278 NB: the types in insts must be correctly instantiated already, 
282 i.e. Tinsts is not applied to insts. 
279 i.e. Tinsts is not applied to insts. 
283 *) 
280 *) 
284 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
281 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
285 let val {maxidx,thy,...} = rep_thm st 
282 let val {maxidx,thy,...} = rep_thm st 
286 val paramTs = map #2 (params_of_state st i) 
283 val paramTs = map #2 (params_of_state i st) 
287 and inc = maxidx+1 
284 and inc = maxidx+1 
288 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
285 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs> Logic.incr_tvar inc T) 
289 (*lift only Var, not term, which must be lifted already*) 
286 (*lift only Var, not term, which must be lifted already*) 
290 fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) 
287 fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) 
291 fun liftTpair (((a, i), S), T) = 
288 fun liftTpair (((a, i), S), T) = 