# HG changeset patch
# User wenzelm
# Date 1303064710 -7200
# Node ID c113db12bf8b91fbb07b8b84549b99fa05c41e7a
# Parent  c3abf2c3f541566afe9af1725c9756b8958f9bd4
tuned -- order in memory according to variance;

diff -r c3abf2c3f541 -r c113db12bf8b src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Apr 17 20:15:46 2011 +0200
+++ b/src/Pure/General/markup.ML	Sun Apr 17 20:25:10 2011 +0200
@@ -172,7 +172,7 @@
 val (bindingN, binding) = markup_string "binding" nameN;
 
 val entityN = "entity";
-fun entity kind name = (entityN, [(kindN, kind), (nameN, name)]);
+fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
 
 val defN = "def";
 val refN = "ref";