diff -r a4ab5d0cccd1 -r 105f40051387 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Fri Oct 02 22:02:54 2009 +0200
+++ b/src/Tools/intuitionistic.ML	Fri Oct 02 22:15:08 2009 +0200
@@ -69,7 +69,6 @@
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 fun modifier name kind kind' att =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)