author | wenzelm |
Sat, 29 Sep 2007 21:39:48 +0200 | |
changeset 24763 | da4a9986eccd |
parent 24762 | 8d7da66b1a2c |
child 24764 | 4c2b872f8cf6 |
--- 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 =