src/Pure/Isar/calculation.ML
changeset 8634 3f34637cb9c0
parent 8588 b7c3f264f8ac
child 8649 dc496bb0638f
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Mar 31 21:54:50 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Mar 31 21:55:27 2000 +0200
     1.3 @@ -91,15 +91,9 @@
     1.4  
     1.5  (* concrete syntax *)
     1.6  
     1.7 -val transN = "trans";
     1.8 -val addN = "add";
     1.9 -val delN = "del";
    1.10 -
    1.11 -fun trans_att add del =
    1.12 -  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
    1.13 -
    1.14  val trans_attr =
    1.15 -  (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
    1.16 + (Attrib.add_del_args trans_add_global trans_del_global,
    1.17 +  Attrib.add_del_args trans_add_local trans_del_local);
    1.18  
    1.19  
    1.20  
    1.21 @@ -181,7 +175,7 @@
    1.22  (** theory setup **)
    1.23  
    1.24  val setup = [GlobalCalculation.init, LocalCalculation.init,
    1.25 -  Attrib.add_attributes [(transN, trans_attr, "declare transitivity rule")]];
    1.26 +  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
    1.27  
    1.28  
    1.29  end;