src/Pure/Isar/context_rules.ML
changeset 56204 f70e69208a8c
parent 53171 a5e54d4d9081
child 56334 6b3739fee456
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Mar 18 13:36:28 2014 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Mar 18 15:29:58 2014 +0100
     1.3 @@ -209,13 +209,13 @@
     1.4      Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
     1.8 + (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
     1.9      "declaration of introduction rule" #>
    1.10 -  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
    1.11 +  Attrib.setup @{binding elim} (add elim_bang elim elim_query)
    1.12      "declaration of elimination rule" #>
    1.13 -  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
    1.14 +  Attrib.setup @{binding dest} (add dest_bang dest dest_query)
    1.15      "declaration of destruction rule" #>
    1.16 -  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
    1.17 +  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    1.18      "remove declaration of intro/elim/dest rule");
    1.19  
    1.20  end;