Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified Consts.dest;
authorwenzelm
Sun, 11 Nov 2007 20:29:05 +0100
changeset 25405 7ac8c93be624
parent 25404 1a58d1c9fe88
child 25406 1aa7927a6759
simplified Consts.dest;
src/Pure/display.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle