# HG changeset patch
# User wenzelm
# Date 1369818398 -7200
# Node ID c8ee9c0a3a648eee62f7f25b541a8cdf38cd1c96
# Parent  b3a5c6f2cb671f598bc207ec7dc20f19b18a9a2a
observe type annotations in print translations as well, notably type_constraint_tr';

diff -r b3a5c6f2cb67 -r c8ee9c0a3a64 src/Pure/Syntax/syntax_phases.ML
--- 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)
diff -r b3a5c6f2cb67 -r c8ee9c0a3a64 src/Pure/Syntax/type_annotation.ML
--- a/src/Pure/Syntax/type_annotation.ML	Wed May 29 10:47:42 2013 +0200
+++ b/src/Pure/Syntax/type_annotation.ML	Wed May 29 11:06:38 2013 +0200
@@ -10,7 +10,6 @@
   val ignore_free_types: term -> term
   val is_ignored: typ -> bool
   val is_omitted: typ -> bool
-  val clean: typ -> typ
   val smash: typ -> typ
   val fastype_of: typ list -> term -> typ
 end;
@@ -29,10 +28,6 @@
 
 fun is_omitted T = is_ignored T orelse T = dummyT;
 
-fun clean (Type ("_ignore_type", [T])) = clean T
-  | clean (Type (a, Ts)) = Type (a, map clean Ts)
-  | clean T = T;
-
 fun smash (Type ("_ignore_type", [_])) = dummyT
   | smash (Type (a, Ts)) = Type (a, map smash Ts)
   | smash T = T;