src/Pure/Isar/rule_cases.ML
changeset 8497 88d7a4f834ff
parent 8427 b19b817522a5
child 8636 635dd6b13028
--- a/src/Pure/Isar/rule_cases.ML	Fri Mar 17 16:28:59 2000 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Mar 17 16:29:35 2000 +0100
@@ -32,7 +32,7 @@
 
 fun name names thm =
   thm
-  |> Drule.untag_rule (casesN, [])
+  |> Drule.untag_rule casesN
   |> Drule.tag_rule (casesN, names);
 
 fun case_names ss = Drule.rule_attribute (K (name ss));