src/Pure/theory.ML

--- a/src/Pure/theory.ML	Sat Sep 29 21:39:47 2007 +0200
+++ b/src/Pure/theory.ML	Sat Sep 29 21:39:48 2007 +0200
@@ -270,10 +270,8 @@
 
 fun check_overloading thy overloaded (c, T) =
   let
-    val declT =
-      (case Sign.const_constraint thy c of
-        NONE => error ("Undeclared constant " ^ quote c)
-      | SOME declT => declT);
+    val declT = Sign.the_const_constraint thy c
+      handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT T;
 
     fun message txt =