# 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;