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.
Added missing default clause | top_const _ = None;
authornipkow
Fri, 17 May 1996 16:22:23 +0200
changeset 1749 8968b2096011
parent 1748 88650ba93c10
child 1750 817a34a54fb0
Added missing default clause | top_const _ = None;
src/Pure/Thy/thm_database.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/thm_database.ML	Fri May 17 16:08:06 1996 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri May 17 16:22:23 1996 +0200
@@ -36,7 +36,8 @@
 
 (* top_const: main constant, ignoring Trueprop *)
 fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
-                                         | _          => None);
+                                         | _          => None)
+  | top_const _ = None;
 
 (*Symtab which associates a constant with a list of theorems that contain the
   constant (theorems are tagged with numbers)*)
isabelle