# HG changeset patch
# User wenzelm
# Date 954532573 -7200
# Node ID 635dd6b130285341a502fba780e94d66b1dd911c
# Parent  2f699cd7b8d7bd5a63399e0bc1ef8c97fcd85116
params: preserve case names;

diff -r 2f699cd7b8d7 -r 635dd6b13028 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Mar 31 21:55:51 2000 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri Mar 31 21:56:13 2000 +0200
@@ -61,7 +61,8 @@
 (* params *)
 
 fun rename_params xss thm =
-  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss));
+  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss))
+  |> name (get thm);
 
 fun params xss = Drule.rule_attribute (K (rename_params xss));