src/Pure/Isar/context_rules.ML
changeset 30529 23d1892f8015
parent 29606 fedb8be05f24
child 32091 30e2ffbba718
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -29,9 +29,8 @@
     1.4    val elim_query: int option -> attribute
     1.5    val dest_query: int option -> attribute
     1.6    val rule_del: attribute
     1.7 -  val add_args:
     1.8 -    (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
     1.9 -    Attrib.src -> attribute
    1.10 +  val add: (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
    1.11 +    attribute context_parser
    1.12  end;
    1.13  
    1.14  structure ContextRules: CONTEXT_RULES =
    1.15 @@ -203,17 +202,18 @@
    1.16  
    1.17  (* concrete syntax *)
    1.18  
    1.19 -fun add_args a b c = Attrib.syntax
    1.20 +fun add a b c x =
    1.21    (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
    1.22 -    Scan.option OuterParse.nat) >> (fn (f, n) => f n));
    1.23 +    Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
    1.24  
    1.25 -val rule_atts =
    1.26 - [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
    1.27 -  ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
    1.28 -  ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
    1.29 -  ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    1.30 -    "remove declaration of intro/elim/dest rule")];
    1.31 -
    1.32 -val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
    1.33 +val _ = Context.>> (Context.map_theory
    1.34 + (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
    1.35 +    "declaration of introduction rule" #>
    1.36 +  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
    1.37 +    "declaration of elimination rule" #>
    1.38 +  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
    1.39 +    "declaration of destruction rule" #>
    1.40 +  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
    1.41 +    "remove declaration of intro/elim/dest rule"));
    1.42  
    1.43  end;