src/Pure/Isar/attrib.ML
changeset 34986 7f7939c9370f
parent 33666 e49bfeb0d822
child 35021 c839a4c670c6
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Jan 27 14:03:08 2010 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Jan 30 16:56:28 2010 +0100
     1.3 @@ -288,6 +288,8 @@
     1.4    setup (Binding.name "folded") folded "folded definitions" #>
     1.5    setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     1.6      "number of consumed facts" #>
     1.7 +  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
     1.8 +    "number of equality constraints" #>
     1.9    setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    1.10      "named rule cases" #>
    1.11    setup (Binding.name "case_conclusion")