simplified Consts.dest;
authorwenzelm
Sun Nov 11 20:29:05 2007 +0100 (2007-11-11)
changeset 254057ac8c93be624
parent 25404 1a58d1c9fe88
child 25406 1aa7927a6759
simplified Consts.dest;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sun Nov 11 20:29:04 2007 +0100
     1.2 +++ b/src/Pure/display.ML	Sun Nov 11 20:29:05 2007 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
     1.5  
     1.6      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     1.7 -    val abbrevs = map_filter (fn (c, (ty, SOME (t, _))) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     1.8 +    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     1.9      val cnstrs = NameSpace.extern_table constraints;
    1.10  
    1.11      val axms = NameSpace.extern_table axioms;