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