src/Pure/Isar/context_rules.ML
changeset 18692 2270e25e9128
parent 18667 85d04c28224a
child 18708 4b3dadb4fe33
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Jan 15 19:58:54 2006 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Jan 15 19:58:55 2006 +0100
     1.3 @@ -30,6 +30,8 @@
     1.4    val elim_query: int option -> Context.generic attribute
     1.5    val dest_query: int option -> Context.generic attribute
     1.6    val rule_del: Context.generic attribute
     1.7 +  val add_args: (int option -> 'a attribute) -> (int option -> 'a attribute) ->
     1.8 +    (int option -> 'a attribute) -> Attrib.src -> 'a attribute
     1.9  end;
    1.10  
    1.11  structure ContextRules: CONTEXT_RULES =
    1.12 @@ -207,11 +209,9 @@
    1.13  (* concrete syntax *)
    1.14  
    1.15  fun add_args a b c x = Attrib.syntax
    1.16 -  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
    1.17 +  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
    1.18      >> (fn (f, n) => f n)) x;
    1.19  
    1.20 -fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
    1.21 -
    1.22  val rule_atts =
    1.23   [("intro", Attrib.common (add_args intro_bang intro intro_query),
    1.24      "declaration of introduction rule"),
    1.25 @@ -219,7 +219,7 @@
    1.26      "declaration of elimination rule"),
    1.27    ("dest", Attrib.common (add_args dest_bang dest dest_query),
    1.28      "declaration of destruction rule"),
    1.29 -  ("rule", Attrib.common (del_args rule_del),
    1.30 +  ("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
    1.31      "remove declaration of intro/elim/dest rule")];
    1.32  
    1.33  val _ = Context.add_setup [Attrib.add_attributes rule_atts];