author | wenzelm |
Fri, 17 Mar 2000 16:29:35 +0100 | |
changeset 8497 | 88d7a4f834ff |
parent 8496 | 7e4a466b18d5 |
child 8498 | e16d6b54332e |
--- 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));