# HG changeset patch
# User wenzelm
# Date 1139534557 -3600
# Node ID 1b11052ad601e97167fcb4ad1a59f4fff4504874
# Parent  ff4e4773cc7ca9878d9e158e2605f71486c17d2c
decode: observe Syntax.constN;

diff -r ff4e4773cc7c -r 1b11052ad601 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Feb 10 02:22:35 2006 +0100
+++ b/src/Pure/type_infer.ML	Fri Feb 10 02:22:37 2006 +0100
@@ -497,6 +497,9 @@
           else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
       | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
       | decode (t $ u) = decode t $ decode u
+      | decode (Const (x, T)) =
+          let val c = (case try (unprefix Syntax.constN) x of SOME c => c | NONE => map_const x)
+          in Const (c, certT T) end
       | decode (Free (x, T)) =
           let val c = map_const x in
             if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
@@ -507,8 +510,7 @@
       | decode (Var (xi, T)) =
           if T = dummyT then Var (xi, get_type xi)
           else constrain (Var (xi, certT T)) (get_type xi)
-      | decode (t as Bound _) = t
-      | decode (Const (c, T)) = Const (map_const c, certT T);
+      | decode (t as Bound _) = t;
   in decode tm end;