517 Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl) |
517 Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl) |
518 in get (rst, n+1, (names,n)::L) end |
518 in get (rst, n+1, (names,n)::L) end |
519 handle TERM _ => get (rst, n+1, L) |
519 handle TERM _ => get (rst, n+1, L) |
520 | U.ERR _ => get (rst, n+1, L); |
520 | U.ERR _ => get (rst, n+1, L); |
521 |
521 |
522 (* Note: rename_params_rule counts from 1, not 0 *) |
522 (* Note: Thm.rename_params_rule counts from 1, not 0 *) |
523 fun rename thm = |
523 fun rename thm = |
524 let val thy = Thm.theory_of_thm thm |
524 let val thy = Thm.theory_of_thm thm |
525 val tych = cterm_of thy |
525 val tych = cterm_of thy |
526 val ants = Logic.strip_imp_prems (Thm.prop_of thm) |
526 val ants = Logic.strip_imp_prems (Thm.prop_of thm) |
527 val news = get (ants,1,[]) |
527 val news = get (ants,1,[]) |
528 in |
528 in |
529 fold rename_params_rule news thm |
529 fold Thm.rename_params_rule news thm |
530 end; |
530 end; |
531 |
531 |
532 |
532 |
533 (*--------------------------------------------------------------------------- |
533 (*--------------------------------------------------------------------------- |
534 * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml) |
534 * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml) |