# HG changeset patch
# User wenzelm
# Date 1003185303 -7200
# Node ID ad12f865b70d5672dc2f3f6d91b02c26f3b2d2b1
# Parent  5f0ab6f5c280f64995ddc03f9328e0359fb12cd4
proper order of kind names;

diff -r 5f0ab6f5c280 -r ad12f865b70d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Oct 16 00:34:34 2001 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 16 00:35:03 2001 +0200
@@ -140,17 +140,18 @@
 
 (** global and local rule data **)
 
-val introK = 0;
-val elimK = 1;
-val intro_bangK = 2;
-val elim_bangK = 3;
+val intro_bangK = 0;
+val elim_bangK = 1;
+val introK = 2;
+val elimK = 3;
 
 local
 
-fun kind_name 0 = "introduction rules (intro)"
-  | kind_name 1 = "elimination rules (elim)"
-  | kind_name 2 = "safe introduction rules (intro!)"
-  | kind_name 3 = "safe elimination rules (elim!)";
+fun kind_name 0 = "safe introduction rules (intro!)"
+  | kind_name 1 = "safe elimination rules (elim!)"
+  | kind_name 2 = "introduction rules (intro)"
+  | kind_name 3 = "elimination rules (elim)"
+  | kind_name _ = "unknown";
 
 fun prt_rules sg (k, rs) =
   Pretty.writeln (Pretty.big_list (kind_name k ^ ":")