equal
deleted
inserted
replaced
121 in Const (c, map_type T) end |
121 in Const (c, map_type T) end |
122 | decode (Free (a, T)) = |
122 | decode (Free (a, T)) = |
123 (case (map_free a, map_const a) of |
123 (case (map_free a, map_const a) of |
124 (SOME x, _) => Free (x, map_type T) |
124 (SOME x, _) => Free (x, map_type T) |
125 | (_, SOME c) => Const (c, map_type T) |
125 | (_, SOME c) => Const (c, map_type T) |
126 | _ => Free (a, map_type T)) |
126 | _ => (if NameSpace.is_qualified a then Const else Free) (a, map_type T)) |
127 | decode (Var (xi, T)) = Var (xi, map_type T) |
127 | decode (Var (xi, T)) = Var (xi, map_type T) |
128 | decode (t as Bound _) = t; |
128 | decode (t as Bound _) = t; |
129 in decode tm end; |
129 in decode tm end; |
130 |
130 |
131 |
131 |