# HG changeset patch
# User wenzelm
# Date 1010705365 -3600
# Node ID d9e0674653b34bba0693cdf3e9f23a701aaa1b4b
# Parent  e29800eba5d10e350eba8052dac53f88b77e2c23
kind: ignore "";

diff -r e29800eba5d1 -r d9e0674653b3 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jan 11 00:28:43 2002 +0100
+++ b/src/Pure/drule.ML	Fri Jan 11 00:29:25 2002 +0100
@@ -278,7 +278,7 @@
   | _ => "unknown");
 
 fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
-fun kind k x = rule_attribute (K (kind_rule k)) x;
+fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
 fun kind_internal x = kind internalK x;
 fun has_internal tags = exists (equal internalK o fst) tags;