# HG changeset patch
# User nipkow
# Date 832342943 -7200
# Node ID 8968b2096011590322a0f4fbbcfd1963fc3ea849
# Parent  88650ba93c10f08f58bb853e15437c69a0f621f9
Added missing default clause   | top_const _ = None;

diff -r 88650ba93c10 -r 8968b2096011 src/Pure/Thy/thm_database.ML
--- 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)*)