# 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));