# HG changeset patch
# User wenzelm
# Date 1372324068 -7200
# Node ID 36497ee02ed8dd4b7bc2e19ea5184e5dd093dc21
# Parent  c45a6939217f919705d6e45ac0361191cce9133d
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;

diff -r c45a6939217f -r 36497ee02ed8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Jun 27 10:35:37 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Jun 27 11:07:48 2013 +0200
@@ -533,15 +533,16 @@
     fun aprop t = Syntax.const "_aprop" $ t;
 
     fun is_prop Ts t =
-      Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
+      Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
+        handle TERM _ => false;
 
     fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun mark _ (t as Const _) = t
       | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
-      | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
-      | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
+      | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
+      | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
       | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
       | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
       | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
@@ -628,7 +629,12 @@
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T0 =
-      let val T = Type_Annotation.smash T0 in
+      let
+        val T =
+          if show_markup andalso not show_types
+          then Type_Annotation.clean T0
+          else Type_Annotation.smash T0;
+      in
         if (show_types orelse show_markup) andalso T <> dummyT then
           Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
             ast_of_termT ctxt trf (term_of_typ ctxt T)]
diff -r c45a6939217f -r 36497ee02ed8 src/Pure/Syntax/type_annotation.ML
--- a/src/Pure/Syntax/type_annotation.ML	Thu Jun 27 10:35:37 2013 +0200
+++ b/src/Pure/Syntax/type_annotation.ML	Thu Jun 27 11:07:48 2013 +0200
@@ -10,6 +10,7 @@
   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;
@@ -28,6 +29,10 @@
 
 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;