# HG changeset patch
# User wenzelm
# Date 1194809345 -3600
# Node ID 7ac8c93be6243b8b2052829068778936f46e13e6
# Parent  1a58d1c9fe88cab5b4b478aacd2ecc10ef1781c8
simplified Consts.dest;

diff -r 1a58d1c9fe88 -r 7ac8c93be624 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Nov 11 20:29:04 2007 +0100
+++ b/src/Pure/display.ML	Sun Nov 11 20:29:05 2007 +0100
@@ -221,7 +221,7 @@
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
-    val abbrevs = map_filter (fn (c, (ty, SOME (t, _))) => SOME (c, (ty, t)) | _ => NONE) cnsts;
+    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = NameSpace.extern_table constraints;
 
     val axms = NameSpace.extern_table axioms;