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