src/Pure/display.ML
changeset 17995 8b9c6af78a67
parent 17704 f776b3bf4126
child 18061 972e3d554eb8
--- a/src/Pure/display.ML	Thu Oct 27 13:54:42 2005 +0200
+++ b/src/Pure/display.ML	Thu Oct 27 13:54:43 2005 +0200
@@ -201,7 +201,7 @@
     val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
     val tdecls = NameSpace.dest_table types;
     val arties = NameSpace.dest_table (Sign.type_space thy, arities);
-    val cnsts = NameSpace.extern_table consts |> map (apsnd fst);
+    val cnsts = NameSpace.extern_table consts |> map (apsnd (fst o fst));
     val cnsts' = NameSpace.extern_table (#1 consts, constraints);
     val axms = NameSpace.extern_table axioms;
     val oras = NameSpace.extern_table oracles;