# HG changeset patch
# User wenzelm
# Date 1191094788 -7200
# Node ID da4a9986eccd246b0e5829361ba112c190d22afb
# Parent  8d7da66b1a2c4bf3ae4bed49408c29b6ba12530f
Sign.the_const_constraint;

diff -r 8d7da66b1a2c -r da4a9986eccd 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 =