220 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
220 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
221 | types'(ixn) = types ixn; |
221 | types'(ixn) = types ixn; |
222 val used = add_term_tvarnames |
222 val used = add_term_tvarnames |
223 (#prop(rep_thm st) $ #prop(rep_thm rule),[]) |
223 (#prop(rep_thm st) $ #prop(rep_thm rule),[]) |
224 val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts |
224 val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts |
225 in instantiate (map lifttvar Tinsts, map liftpair insts) |
225 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) |
226 (lift_rule (st,i) rule) |
226 (lift_rule (st,i) rule) |
227 end; |
227 end; |
228 |
228 |
229 (* |
229 (* |
230 Like lift_inst_rule but takes terms, not strings, where the terms may contain |
230 Like lift_inst_rule but takes terms, not strings, where the terms may contain |
231 Bounds referring to parameters of the subgoal. |
231 Bounds referring to parameters of the subgoal. |
249 and inc = maxidx+1 |
249 and inc = maxidx+1 |
250 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
250 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
251 (*lift only Var, not term, which must be lifted already*) |
251 (*lift only Var, not term, which must be lifted already*) |
252 fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) |
252 fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) |
253 fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) |
253 fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) |
254 in instantiate (map liftTpair Tinsts, map liftpair insts) |
254 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) |
255 (lift_rule (st,i) rule) |
255 (lift_rule (st,i) rule) |
256 end; |
256 end; |
257 |
257 |
258 (*** Resolve after lifting and instantation; may refer to parameters of the |
258 (*** Resolve after lifting and instantation; may refer to parameters of the |
259 subgoal. Fails if "i" is out of range. ***) |
259 subgoal. Fails if "i" is out of range. ***) |
260 |
260 |