changeset 11002 | e33dfe9bde39 |
parent 10886 | f6b16554720d |
child 11764 | fd780dd6e0b4 |
--- a/src/Pure/Isar/rule_cases.ML Tue Jan 30 18:48:33 2001 +0100 +++ b/src/Pure/Isar/rule_cases.ML Tue Jan 30 18:53:46 2001 +0100 @@ -104,8 +104,7 @@ (* params *) -fun rename_params xss thm = - #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss)) +fun rename_params xss thm = foldln Thm.rename_params_rule xss thm |> save thm; fun params xss = Drule.rule_attribute (K (rename_params xss));