--- a/src/Pure/Syntax/syntax_phases.ML Wed May 29 10:47:42 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed May 29 11:06:38 2013 +0200
@@ -621,7 +621,7 @@
in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
- | (const as Const (c, T), ts) => trans c (Type_Annotation.clean T) ts
+ | (const as Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args = ast_of (trf a ctxt T args)