fixed untag;
authorwenzelm
Fri, 17 Mar 2000 16:29:35 +0100
changeset 8497 88d7a4f834ff
parent 8496 7e4a466b18d5
child 8498 e16d6b54332e
fixed untag;
src/Pure/Isar/rule_cases.ML
--- 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));