read_const: include type;

--- a/src/Pure/consts.ML	Tue Nov 07 11:46:46 2006 +0100
+++ b/src/Pure/consts.ML	Tue Nov 07 11:46:47 2006 +0100
@@ -132,8 +132,8 @@
 fun read_const consts raw_c =
   let
     val c = intern consts raw_c;
-    val _ = the_const consts c handle TYPE (msg, _, _) => error msg;
-  in Const (c, dummyT) end;
+    val (((T, _), _), _) = the_const consts c handle TYPE (msg, _, _) => error msg;
+  in Const (c, T) end;
 
 
 (* certify *)