432 | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t |
432 | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t |
433 | get_bno l n (t $ s) = get_bno l n t |
433 | get_bno l n (t $ s) = get_bno l n t |
434 | get_bno l n (Bound m) = (m-length(l),n) |
434 | get_bno l n (Bound m) = (m-length(l),n) |
435 |
435 |
436 (* Not a great way of identifying induction hypothesis! *) |
436 (* Not a great way of identifying induction hypothesis! *) |
437 fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse |
437 fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse |
438 could_unify(x,hd (prems_of @{thm rcall2T})) orelse |
438 Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse |
439 could_unify(x,hd (prems_of @{thm rcall3T})) |
439 Term.could_unify(x,hd (prems_of @{thm rcall3T})) |
440 |
440 |
441 fun IHinst tac rls = SUBGOAL (fn (Bi,i) => |
441 fun IHinst tac rls = SUBGOAL (fn (Bi,i) => |
442 let val bvs = bvars Bi [] |
442 let val bvs = bvars Bi [] |
443 val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) |
443 val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) |
444 val rnames = map (fn x=> |
444 val rnames = map (fn x=> |