# HG changeset patch
# User wenzelm
# Date 953306975 -3600
# Node ID 88d7a4f834ff26b9ddc7c8863e33e726d65610da
# Parent  7e4a466b18d581b45586ec949d9126fe58a0ad36
fixed untag;

diff -r 7e4a466b18d5 -r 88d7a4f834ff 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));