| changeset 61853 | fb7756087101 |
| parent 61834 | 2154e6c8d52d |
| child 63512 | 1c7b1e294fb5 |
--- a/src/Pure/Isar/rule_cases.ML Tue Dec 15 16:57:10 2015 +0100 +++ b/src/Pure/Isar/rule_cases.ML Wed Dec 16 16:31:36 2015 +0100 @@ -404,7 +404,7 @@ |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss |> save th; -fun params xss = Thm.rule_attribute (K (rename_params xss)); +fun params xss = Thm.rule_attribute [] (K (rename_params xss));