# HG changeset patch
# User nipkow
# Date 1312632983 -7200
# Node ID a43ca8ed65645c3aaf78432d6e751e9e67ff3e59
# Parent  2814ff2a6e3e7e2b63eac4f5209afe302c5bf55b
extended user-level attribute case_names with names for case hypotheses

diff -r 2814ff2a6e3e -r a43ca8ed6564 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 01 12:08:53 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Aug 06 14:16:23 2011 +0200
@@ -267,6 +267,22 @@
 val elim_format = Thm.rule_attribute (K Tactic.make_elim);
 
 
+(* case names *)
+
+fun hname NONE = Rule_Cases.case_hypsN
+  | hname (SOME n) = n;
+
+fun case_names cs =
+  Rule_Cases.case_names (map fst cs) #>
+  Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
+
+val hnamesP =
+  Scan.optional
+    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
+    []
+
+val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
+
 (* misc rules *)
 
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -300,7 +316,7 @@
     "number of consumed facts" #>
   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
     "number of equality constraints" #>
-  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
+  setup (Binding.name "case_names") (case_namesP >> case_names)
     "named rule cases" #>
   setup (Binding.name "case_conclusion")
     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)