src/Pure/display.ML
changeset 21721 908a93216f00
parent 21646 c07b5b0e8492
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/display.ML	Sat Dec 09 18:05:39 2006 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Dec 09 18:05:40 2006 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4      val arties = dest_table (Sign.type_space thy, arities);
     1.5      val cnsts = extern_table constants;
     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 = extern_table constraints;
    1.10      val axms = extern_table axioms;
    1.11      val oras = extern_table oracles;