| changeset 12710 | d9e0674653b3 |
| parent 12527 | d6c91bc3e49c |
| child 12719 | 41e0d086f8b6 |
--- 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;