src/Pure/theory.ML
changeset 24763 da4a9986eccd
parent 24708 d9b00117365e
child 24966 70111480b84b
     1.1 --- a/src/Pure/theory.ML	Sat Sep 29 21:39:47 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Sep 29 21:39:48 2007 +0200
     1.3 @@ -270,10 +270,8 @@
     1.4  
     1.5  fun check_overloading thy overloaded (c, T) =
     1.6    let
     1.7 -    val declT =
     1.8 -      (case Sign.const_constraint thy c of
     1.9 -        NONE => error ("Undeclared constant " ^ quote c)
    1.10 -      | SOME declT => declT);
    1.11 +    val declT = Sign.the_const_constraint thy c
    1.12 +      handle TYPE (msg, _, _) => error msg;
    1.13      val T' = Logic.varifyT T;
    1.14  
    1.15      fun message txt =