# HG changeset patch
# User wenzelm
# Date 1162896407 -3600
# Node ID dfe338ec9f9ca482bbbe226a796aba86eaecd088
# Parent  1e96553668c6269c9a014cdbf33016d520e1edd1
read_const: include type;

diff -r 1e96553668c6 -r dfe338ec9f9c src/Pure/consts.ML
--- 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 *)