proper order of kind names;
authorwenzelm
Tue Oct 16 00:35:03 2001 +0200 (2001-10-16)
changeset 11794ad12f865b70d
parent 11793 5f0ab6f5c280
child 11795 12a0fb3ac366
proper order of kind names;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Oct 16 00:34:34 2001 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Oct 16 00:35:03 2001 +0200
     1.3 @@ -140,17 +140,18 @@
     1.4  
     1.5  (** global and local rule data **)
     1.6  
     1.7 -val introK = 0;
     1.8 -val elimK = 1;
     1.9 -val intro_bangK = 2;
    1.10 -val elim_bangK = 3;
    1.11 +val intro_bangK = 0;
    1.12 +val elim_bangK = 1;
    1.13 +val introK = 2;
    1.14 +val elimK = 3;
    1.15  
    1.16  local
    1.17  
    1.18 -fun kind_name 0 = "introduction rules (intro)"
    1.19 -  | kind_name 1 = "elimination rules (elim)"
    1.20 -  | kind_name 2 = "safe introduction rules (intro!)"
    1.21 -  | kind_name 3 = "safe elimination rules (elim!)";
    1.22 +fun kind_name 0 = "safe introduction rules (intro!)"
    1.23 +  | kind_name 1 = "safe elimination rules (elim!)"
    1.24 +  | kind_name 2 = "introduction rules (intro)"
    1.25 +  | kind_name 3 = "elimination rules (elim)"
    1.26 +  | kind_name _ = "unknown";
    1.27  
    1.28  fun prt_rules sg (k, rs) =
    1.29    Pretty.writeln (Pretty.big_list (kind_name k ^ ":")