--- a/src/Pure/Syntax/type_ext.ML Wed Apr 28 19:43:45 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML Thu Apr 29 11:00:32 2010 +0200
@@ -120,11 +120,14 @@
| decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
- let val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (map_const a))
- in Const (c, T) end
+ (case try Lexicon.unmark_fixed a of
+ SOME x => Free (x, T)
+ | NONE =>
+ let val c =
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (map_const a))
+ in Const (c, T) end)
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
(SOME x, _) => Free (x, T)