src/Pure/Isar/attrib.ML
changeset 44046 a43ca8ed6564
parent 43347 f18cf88453d6
child 44053 3cc902f81a26
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 01 12:08:53 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Aug 06 14:16:23 2011 +0200
     1.3 @@ -267,6 +267,22 @@
     1.4  val elim_format = Thm.rule_attribute (K Tactic.make_elim);
     1.5  
     1.6  
     1.7 +(* case names *)
     1.8 +
     1.9 +fun hname NONE = Rule_Cases.case_hypsN
    1.10 +  | hname (SOME n) = n;
    1.11 +
    1.12 +fun case_names cs =
    1.13 +  Rule_Cases.case_names (map fst cs) #>
    1.14 +  Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
    1.15 +
    1.16 +val hnamesP =
    1.17 +  Scan.optional
    1.18 +    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
    1.19 +    []
    1.20 +
    1.21 +val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
    1.22 +
    1.23  (* misc rules *)
    1.24  
    1.25  val no_vars = Thm.rule_attribute (fn context => fn th =>
    1.26 @@ -300,7 +316,7 @@
    1.27      "number of consumed facts" #>
    1.28    setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    1.29      "number of equality constraints" #>
    1.30 -  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    1.31 +  setup (Binding.name "case_names") (case_namesP >> case_names)
    1.32      "named rule cases" #>
    1.33    setup (Binding.name "case_conclusion")
    1.34      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)