explicit support for type annotations within printed syntax trees;
eliminated obsolete show_free_types;

--- a/src/Pure/ROOT	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/ROOT	Tue May 28 23:06:32 2013 +0200
@@ -174,6 +174,7 @@
     "Syntax/syntax_phases.ML"
     "Syntax/syntax_trans.ML"
     "Syntax/term_position.ML"
+    "Syntax/type_annotation.ML"
     "System/command_line.ML"
     "System/invoke_scala.ML"
     "System/isabelle_process.ML"

--- a/src/Pure/ROOT.ML	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/ROOT.ML	Tue May 28 23:06:32 2013 +0200
@@ -121,6 +121,7 @@
 
 (* inner syntax *)
 
+use "Syntax/type_annotation.ML";
 use "Syntax/term_position.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/ast.ML";

--- a/src/Pure/Syntax/printer.ML	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue May 28 23:06:32 2013 +0200
@@ -9,7 +9,6 @@
   val show_brackets: bool Config.T
   val show_types: bool Config.T
   val show_sorts: bool Config.T
-  val show_free_types: bool Config.T
   val show_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
@@ -58,8 +57,6 @@
 val show_sorts_raw = Config.declare_option "show_sorts";
 val show_sorts = Config.bool show_sorts_raw;
 
-val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
-
 val show_markup_default = Unsynchronized.ref false;
 val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
 val show_markup = Config.bool show_markup_raw;

--- a/src/Pure/Syntax/syntax_phases.ML	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue May 28 23:06:32 2013 +0200
@@ -533,7 +533,7 @@
     fun aprop t = Syntax.const "_aprop" $ t;
 
     fun is_prop Ts t =
-      fastype_of1 (Ts, t) = propT handle TERM _ => false;
+      Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
 
     fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
@@ -554,21 +554,18 @@
 
 fun prune_types ctxt tm =
   let
-    val show_free_types = Config.get ctxt show_free_types;
+    fun regard t t' seen =
+      if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
+      else if member (op aconv) seen t then (t', seen)
+      else (t, t :: seen);
 
-    fun prune (t_seen as (Const _, _)) = t_seen
-      | prune (t as Free (x, ty), seen) =
-          if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
-          else (t, t :: seen)
-      | prune (t as Var (xi, ty), seen) =
-          if ty = dummyT then (t, seen)
-          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
-          else (t, t :: seen)
-      | prune (t_seen as (Bound _, _)) = t_seen
-      | prune (Abs (x, ty, t), seen) =
+    fun prune (t as Const _, seen) = (t, seen)
+      | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
+      | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
+      | prune (t as Bound _, seen) = (t, seen)
+      | prune (Abs (x, T, t), seen) =
           let val (t', seen') = prune (t, seen);
-          in (Abs (x, ty, t'), seen') end
+          in (Abs (x, T, t'), seen') end
       | prune (t1 $ t2, seen) =
           let
             val (t1', seen') = prune (t1, seen);
@@ -624,17 +621,19 @@
           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 T ts
+      | (const as Const (c, T), ts) => trans c (Type_Annotation.clean 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)
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
-    and constrain t T =
-      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)]
-      else simple_ast_of ctxt t;
+    and constrain t T0 =
+      let val T = 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)]
+        else simple_ast_of ctxt t
+      end;
   in
     tm
     |> mark_aprop

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/type_annotation.ML	Tue May 28 23:06:32 2013 +0200
@@ -0,0 +1,65 @@
+(*  Title:      Pure/Syntax/type_annotation.ML
+    Author:     Makarius
+
+Type annotations within syntax trees, notably for pretty printing.
+*)
+
+signature TYPE_ANNOTATION =
+sig
+  val ignore_type: typ -> typ
+  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;
+
+structure Type_Annotation: TYPE_ANNOTATION =
+struct
+
+(* annotations *)
+
+fun ignore_type T = Type ("_ignore_type", [T]);
+
+val ignore_free_types = Term.map_aterms (fn Free (x, T) => Free (x, ignore_type T) | a => a);
+
+fun is_ignored (Type ("_ignore_type", _)) = true
+  | is_ignored _ = false;
+
+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;
+
+
+(* determine type -- propagate annotations *)
+
+local
+
+fun dest_fun ignored (Type ("fun", [_, T])) = SOME ((ignored ? ignore_type) T)
+  | dest_fun _ (Type ("_ignore_type", [T])) = dest_fun true T
+  | dest_fun _ _ = NONE;
+
+in
+
+fun fastype_of Ts (t $ u) =
+      (case dest_fun false (fastype_of Ts t) of
+        SOME T => T
+      | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
+  | fastype_of _ (Const (_, T)) = T
+  | fastype_of _ (Free (_, T)) = T
+  | fastype_of _ (Var (_, T)) = T
+  | fastype_of Ts (Bound i) =
+      (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
+  | fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
+
+end;
+
+end;
+

--- a/src/Pure/goal_display.ML	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/goal_display.ML	Tue May 28 23:06:32 2013 +0200
@@ -70,7 +70,6 @@
 fun pretty_goals ctxt0 state =
   let
     val ctxt = ctxt0
-      |> Config.put show_free_types false
       |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
       |> Config.put show_sorts false;
 
@@ -82,7 +81,7 @@
 
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
-    val prt_term = Syntax.pretty_term ctxt;
+    val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
 
     fun prt_atoms prt prtT (X, xs) = Pretty.block
       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",

--- a/src/Pure/pure_thy.ML	Tue May 28 16:29:11 2013 +0200
+++ b/src/Pure/pure_thy.ML	Tue May 28 23:06:32 2013 +0200
@@ -81,6 +81,7 @@
     ("",            typ "prop' => prop'",              Delimfix "'(_')"),
     ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
     ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
+    ("_ignore_type", typ "'a",                         NoSyn),
     ("",            typ "tid_position => type",        Delimfix "_"),
     ("",            typ "tvar_position => type",       Delimfix "_"),
     ("",            typ "type_name => type",           Delimfix "_"),