src/Pure/Isar/rule_cases.ML
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));