decode: observe Syntax.constN;
authorwenzelm
Fri Feb 10 02:22:37 2006 +0100 (2006-02-10)
changeset 189961b11052ad601
parent 18995 ff4e4773cc7c
child 18997 3229c88bbbdf
decode: observe Syntax.constN;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Fri Feb 10 02:22:35 2006 +0100
     1.2 +++ b/src/Pure/type_infer.ML	Fri Feb 10 02:22:37 2006 +0100
     1.3 @@ -497,6 +497,9 @@
     1.4            else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
     1.5        | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
     1.6        | decode (t $ u) = decode t $ decode u
     1.7 +      | decode (Const (x, T)) =
     1.8 +          let val c = (case try (unprefix Syntax.constN) x of SOME c => c | NONE => map_const x)
     1.9 +          in Const (c, certT T) end
    1.10        | decode (Free (x, T)) =
    1.11            let val c = map_const x in
    1.12              if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
    1.13 @@ -507,8 +510,7 @@
    1.14        | decode (Var (xi, T)) =
    1.15            if T = dummyT then Var (xi, get_type xi)
    1.16            else constrain (Var (xi, certT T)) (get_type xi)
    1.17 -      | decode (t as Bound _) = t
    1.18 -      | decode (Const (c, T)) = Const (map_const c, certT T);
    1.19 +      | decode (t as Bound _) = t;
    1.20    in decode tm end;
    1.21  
    1.22