params: preserve case names;
authorwenzelm
Fri, 31 Mar 2000 21:56:13 +0200
changeset 8636 635dd6b13028
parent 8635 2f699cd7b8d7
child 8637 e86e49aa1631
params: preserve case names;
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));