equal
deleted
inserted
replaced
402 fun rename_params xss th = |
402 fun rename_params xss th = |
403 th |
403 th |
404 |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss |
404 |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss |
405 |> save th; |
405 |> save th; |
406 |
406 |
407 fun params xss = Thm.rule_attribute (K (rename_params xss)); |
407 fun params xss = Thm.rule_attribute [] (K (rename_params xss)); |
408 |
408 |
409 |
409 |
410 |
410 |
411 (** mutual_rule **) |
411 (** mutual_rule **) |
412 |
412 |