kind: ignore "";
authorwenzelm
Fri Jan 11 00:29:25 2002 +0100 (2002-01-11 ago)
changeset 12710d9e0674653b3
parent 12709 e29800eba5d1
child 12711 6a9412dd7d24
kind: ignore "";
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Jan 11 00:28:43 2002 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Jan 11 00:29:25 2002 +0100
     1.3 @@ -278,7 +278,7 @@
     1.4    | _ => "unknown");
     1.5  
     1.6  fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
     1.7 -fun kind k x = rule_attribute (K (kind_rule k)) x;
     1.8 +fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
     1.9  fun kind_internal x = kind internalK x;
    1.10  fun has_internal tags = exists (equal internalK o fst) tags;
    1.11