# HG changeset patch
# User wenzelm
# Date 1302087493 -7200
# Node ID 29e3967550d5e43a33a5ccbd6589b07fa3103be7
# Parent  15bba1fb39d12ecf10cc7b16c72175631099de88
moved unparse material to syntax_phases.ML;

diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Groups.thy	Wed Apr 06 12:58:13 2011 +0200
@@ -130,7 +130,7 @@
     if not (null ts) orelse T = dummyT
       orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
     then raise Match
-    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T);
 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
 *} -- {* show types that are presumably too general *}
 
diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:58:13 2011 +0200
@@ -37,7 +37,7 @@
 typed_print_translation {*
 let
   fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
-    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
+    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
 in [(@{const_syntax card}, card_univ_tr')]
 end
 *}
diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -72,7 +72,9 @@
 fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
       let val t' =
         if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
-        else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
+        else
+          Syntax.const Syntax.constrainC $ syntax_numeral t $
+            Syntax_Phases.term_of_typ show_sorts T
       in list_comb (t', ts) end
   | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
       if T = dummyT then list_comb (syntax_numeral t, ts)
diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Tools/record.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -708,7 +708,7 @@
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
-                    val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
+                    val term_of_typ = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
                     val alphas' =
                       map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
 
@@ -819,7 +819,7 @@
     val T = decode_type thy t;
     val varifyT = varifyT (Term.maxidx_of_typ T);
 
-    val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
+    val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
 
     fun strip_fields T =
       (case T of
@@ -865,7 +865,7 @@
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
-      in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
+      in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in
diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Typerep.thy	Wed Apr 06 12:58:13 2011 +0200
@@ -36,7 +36,7 @@
           (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
           (Const (@{const_syntax TYPE}, _) :: ts) =
         Term.list_comb
-          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
+          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
     | typerep_tr' _ T ts = raise Match;
 in [(@{const_syntax typerep}, typerep_tr')] end
 *}
diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 12:58:13 2011 +0200
@@ -309,7 +309,7 @@
       case T of
         Type (@{type_name fun}, [_, T']) =>
           if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
-          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ show_sorts T'
       | T' => if T' = dummyT then t' else raise Match
     end;
 in [(@{const_syntax of_num}, num_tr')] end
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -23,17 +23,12 @@
   val show_question_marks_raw: Config.raw
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
+  val apply_trans: 'a -> ('a -> 'b -> 'c) list -> 'b -> 'c
 end;
 
 signature PRINTER =
 sig
   include PRINTER0
-  val sort_to_ast: Proof.context ->
-    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
-  val typ_to_ast: Proof.context ->
-    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
-  val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
-    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
@@ -52,7 +47,6 @@
 structure Printer: PRINTER =
 struct
 
-
 (** options for printing **)
 
 val show_brackets_default = Unsynchronized.ref false;
@@ -81,150 +75,6 @@
 
 
 
-(** misc utils **)
-
-(* apply print (ast) translation function *)
-
-fun apply_trans ctxt fns args =
-  let
-    fun app_first [] = raise Match
-      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
-  in app_first fns end;
-
-fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
-
-
-(* simple_ast_of *)
-
-fun simple_ast_of ctxt =
-  let
-    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
-    fun ast_of (Const (c, _)) = Ast.Constant c
-      | ast_of (Free (x, _)) = Ast.Variable x
-      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
-      | ast_of (t as _ $ _) =
-          let val (f, args) = strip_comb t
-          in Ast.mk_appl (ast_of f) (map ast_of args) end
-      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
-      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
-  in ast_of end;
-
-
-
-(** sort_to_ast, typ_to_ast **)
-
-fun ast_of_termT ctxt trf tm =
-  let
-    val ctxt' = Config.put show_sorts false ctxt;
-    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
-      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
-      | ast_of (Const (a, _)) = trans a []
-      | ast_of (t as _ $ _) =
-          (case strip_comb t of
-            (Const (a, _), args) => trans a args
-          | (f, args) => Ast.Appl (map ast_of (f :: args)))
-      | ast_of t = simple_ast_of ctxt t
-    and trans a args =
-      ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
-        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
-  in ast_of tm end;
-
-fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T =
-  ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
-
-
-
-(** term_to_ast **)
-
-fun term_to_ast idents consts ctxt trf tm =
-  let
-    val show_types =
-      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
-      Config.get ctxt show_all_types;
-    val show_sorts = Config.get ctxt show_sorts;
-    val show_structs = Config.get ctxt show_structs;
-    val show_free_types = Config.get ctxt show_free_types;
-    val show_all_types = Config.get ctxt show_all_types;
-
-    val {structs, fixes} = idents;
-
-    fun mark_atoms ((t as Const (c, T)) $ u) =
-          if member (op =) Syn_Ext.standard_token_markers c
-          then t $ u else mark_atoms t $ mark_atoms u
-      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
-      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
-      | mark_atoms (t as Const (c, T)) =
-          if member (op =) consts c then t
-          else Const (Lexicon.mark_const c, T)
-      | mark_atoms (t as Free (x, T)) =
-          let val i = find_index (fn s => s = x) structs + 1 in
-            if i = 0 andalso member (op =) fixes x then
-              Const (Lexicon.mark_fixed x, T)
-            else if i = 1 andalso not show_structs then
-              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
-            else Lexicon.const "_free" $ t
-          end
-      | mark_atoms (t as Var (xi, T)) =
-          if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
-          else Lexicon.const "_var" $ t
-      | mark_atoms a = a;
-
-    fun prune_typs (t_seen as (Const _, _)) = t_seen
-      | prune_typs (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 (Lexicon.free x, seen)
-          else (t, t :: seen)
-      | prune_typs (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 (Lexicon.var xi, seen)
-          else (t, t :: seen)
-      | prune_typs (t_seen as (Bound _, _)) = t_seen
-      | prune_typs (Abs (x, ty, t), seen) =
-          let val (t', seen') = prune_typs (t, seen);
-          in (Abs (x, ty, t'), seen') end
-      | prune_typs (t1 $ t2, seen) =
-          let
-            val (t1', seen') = prune_typs (t1, seen);
-            val (t2', seen'') = prune_typs (t2, seen');
-          in (t1' $ t2', seen'') end;
-
-    fun ast_of tm =
-      (case strip_comb tm of
-        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
-      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
-      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
-      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
-      | (Const ("_idtdummy", T), ts) =>
-          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
-      | (const as Const (c, T), ts) =>
-          if show_all_types
-          then Ast.mk_appl (constrain const T) (map ast_of ts)
-          else trans c T ts
-      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
-
-    and trans a T args =
-      ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
-        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
-
-    and constrain t T =
-      if show_types andalso T <> dummyT then
-        Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
-          ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
-      else simple_ast_of ctxt t;
-  in
-    tm
-    |> Syn_Trans.prop_tr'
-    |> show_types ? (#1 o prune_typs o rpair [])
-    |> mark_atoms
-    |> ast_of
-  end;
-
-
-
 (** type prtabs **)
 
 datatype symb =
@@ -311,6 +161,12 @@
 
 (** pretty term or typ asts **)
 
+fun apply_trans ctxt fns args =
+  let
+    fun app_first [] = raise Match
+      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
+  in app_first fns end;
+
 fun is_chain [Block (_, pr)] = is_chain pr
   | is_chain [Arg _] = true
   | is_chain _  = false;
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -20,6 +20,7 @@
     string -> (string * (Proof.context -> string -> Pretty.T)) list ->
     (string * string * (Proof.context -> string -> Pretty.T)) list
   val standard_token_classes: string list
+  val standard_token_markers: string list
 end;
 
 signature SYN_EXT =
@@ -83,7 +84,6 @@
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
-  val standard_token_markers: string list
   val pure_ext: syn_ext
 end;
 
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -42,7 +42,6 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (Ast.ast list -> Ast.ast)) list
-  val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
   val struct_trfuns: string list ->
     (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
@@ -354,15 +353,6 @@
   | idtyp_ast_tr' _ _ = raise Match;
 
 
-(* type propositions *)
-
-fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
-      Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
-  | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
-      Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
-  | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
-
-
 (* meta propositions *)
 
 fun prop_tr' tm =
@@ -408,20 +398,6 @@
     | _ => raise Match);
 
 
-(* type reflection *)
-
-fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
-      Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
-  | type_tr' _ _ _ = raise Match;
-
-
-(* type constraints *)
-
-fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
-      Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
-  | type_constraint_tr' _ _ _ = raise Match;
-
-
 (* dependent / nondependent quantifiers *)
 
 fun var_abs mark (x, T, b) =
@@ -533,11 +509,6 @@
     ("\\<^const>==>", impl_ast_tr'),
     ("_index", index_ast_tr')]);
 
-val pure_trfunsT =
- [("_type_prop", type_prop_tr'),
-  ("\\<^const>TYPE", type_tr'),
-  ("_type_constraint_", type_constraint_tr')];
-
 fun struct_trfuns structs =
   ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
 
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -95,6 +95,9 @@
   val string_of_sort_global: theory -> sort -> string
   val pp: Proof.context -> Pretty.pp
   val pp_global: theory -> Pretty.pp
+  val lookup_tokentr:
+    (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list ->
+      string list -> string -> (Proof.context -> string -> Pretty.T) option
   type ruletab
   type syntax
   val rep_syntax: syntax ->
@@ -135,13 +138,6 @@
     Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val is_const: syntax -> string -> bool
-  val standard_unparse_sort: {extern_class: string -> xstring} ->
-    Proof.context -> syntax -> sort -> Pretty.T
-  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
-    Proof.context -> syntax -> typ -> Pretty.T
-  val standard_unparse_term: {structs: string list, fixes: string list} ->
-    {extern_class: string -> xstring, extern_type: string -> xstring,
-      extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   val update_trfuns:
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
@@ -415,7 +411,6 @@
 
 (* print (ast) translations *)
 
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
 fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
 fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
@@ -425,12 +420,14 @@
 (** tables of token translation functions **)
 
 fun lookup_tokentr tabs modes =
-  let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
+  let val trs =
+    distinct (eq_fst (op = : string * string -> bool))
+      (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   in fn c => Option.map fst (AList.lookup (op =) trs c) end;
 
 fun merge_tokentrtabs tabs1 tabs2 =
   let
-    fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
+    fun eq_tr ((c1, (_, s1: stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
 
     fun name (s, _) = implode (tl (Symbol.explode s));
 
@@ -754,37 +751,6 @@
 
 
 
-(** unparse terms, typs, sorts **)
-
-local
-
-fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
-  let
-    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
-    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
-  in
-    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
-      (lookup_tokentr tokentrtab (print_mode_value ()))
-      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
-  end;
-
-in
-
-fun standard_unparse_sort {extern_class} ctxt syn =
-  unparse_t (K Printer.sort_to_ast)
-    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
-    Markup.sort ctxt syn false;
-
-fun standard_unparse_typ extern ctxt syn =
-  unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-
-fun standard_unparse_term idents extern =
-  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-
-end;
-
-
-
 (** modify syntax **)
 
 fun ext_syntax f decls = update_syntax mode_default (f decls);
@@ -813,6 +779,5 @@
 
 forget_structure "Syn_Ext";
 forget_structure "Type_Ext";
-forget_structure "Syn_Trans";
 forget_structure "Mixfix";
-forget_structure "Printer";
+
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -12,6 +12,7 @@
   val decode_term: Proof.context ->
     Position.reports * term Exn.result -> Position.reports * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
+  val term_of_typ: bool -> typ -> term
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
@@ -390,17 +391,214 @@
 
 
 
+(** encode parse trees **)
+
+(* term_of_sort *)
+
+fun term_of_sort S =
+  let
+    val class = Lexicon.const o Lexicon.mark_class;
+
+    fun classes [c] = class c
+      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
+  in
+    (case S of
+      [] => Lexicon.const "_topsort"
+    | [c] => class c
+    | cs => Lexicon.const "_sort" $ classes cs)
+  end;
+
+
+(* term_of_typ *)
+
+fun term_of_typ show_sorts ty =
+  let
+    fun of_sort t S =
+      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
+      else t;
+
+    fun term_of (Type (a, Ts)) =
+          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
+      | term_of (TFree (x, S)) =
+          if is_some (Lexicon.decode_position x) then Lexicon.free x
+          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
+      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
+  in term_of ty end;
+
+
+(* simple_ast_of *)
+
+fun simple_ast_of ctxt =
+  let
+    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
+    fun ast_of (Const (c, _)) = Ast.Constant c
+      | ast_of (Free (x, _)) = Ast.Variable x
+      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
+      | ast_of (t as _ $ _) =
+          let val (f, args) = strip_comb t
+          in Ast.mk_appl (ast_of f) (map ast_of args) end
+      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+  in ast_of end;
+
+
+(* sort_to_ast and typ_to_ast *)
+
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
+
+fun ast_of_termT ctxt trf tm =
+  let
+    val ctxt' = Config.put show_sorts false ctxt;
+    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
+      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
+      | ast_of (Const (a, _)) = trans a []
+      | ast_of (t as _ $ _) =
+          (case strip_comb t of
+            (Const (a, _), args) => trans a args
+          | (f, args) => Ast.Appl (map ast_of (f :: args)))
+      | ast_of t = simple_ast_of ctxt t
+    and trans a args =
+      ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args)
+        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
+  in ast_of tm end;
+
+fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ (Config.get ctxt show_sorts) T);
+
+
+(* term_to_ast *)
+
+fun term_to_ast idents consts ctxt trf tm =
+  let
+    val show_types =
+      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+      Config.get ctxt show_all_types;
+    val show_sorts = Config.get ctxt show_sorts;
+    val show_structs = Config.get ctxt show_structs;
+    val show_free_types = Config.get ctxt show_free_types;
+    val show_all_types = Config.get ctxt show_all_types;
+
+    val {structs, fixes} = idents;
+
+    fun mark_atoms ((t as Const (c, T)) $ u) =
+          if member (op =) Syntax.standard_token_markers c
+          then t $ u else mark_atoms t $ mark_atoms u
+      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+      | mark_atoms (t as Const (c, T)) =
+          if member (op =) consts c then t
+          else Const (Lexicon.mark_const c, T)
+      | mark_atoms (t as Free (x, T)) =
+          let val i = find_index (fn s => s = x) structs + 1 in
+            if i = 0 andalso member (op =) fixes x then
+              Const (Lexicon.mark_fixed x, T)
+            else if i = 1 andalso not show_structs then
+              Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+            else Lexicon.const "_free" $ t
+          end
+      | mark_atoms (t as Var (xi, T)) =
+          if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
+          else Lexicon.const "_var" $ t
+      | mark_atoms a = a;
+
+    fun prune_typs (t_seen as (Const _, _)) = t_seen
+      | prune_typs (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 (Lexicon.free x, seen)
+          else (t, t :: seen)
+      | prune_typs (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 (Lexicon.var xi, seen)
+          else (t, t :: seen)
+      | prune_typs (t_seen as (Bound _, _)) = t_seen
+      | prune_typs (Abs (x, ty, t), seen) =
+          let val (t', seen') = prune_typs (t, seen);
+          in (Abs (x, ty, t'), seen') end
+      | prune_typs (t1 $ t2, seen) =
+          let
+            val (t1', seen') = prune_typs (t1, seen);
+            val (t2', seen'') = prune_typs (t2, seen');
+          in (t1' $ t2', seen'') end;
+
+    fun ast_of tm =
+      (case strip_comb tm of
+        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
+      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
+          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
+          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
+          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+      | (Const ("_idtdummy", T), ts) =>
+          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
+      | (const as Const (c, T), ts) =>
+          if show_all_types
+          then Ast.mk_appl (constrain const T) (map ast_of ts)
+          else trans c T ts
+      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
+
+    and trans a T args =
+      ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args)
+        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
+
+    and constrain t T =
+      if show_types andalso T <> dummyT then
+        Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
+          ast_of_termT ctxt trf (term_of_typ show_sorts T)]
+      else simple_ast_of ctxt t;
+  in
+    tm
+    |> Syn_Trans.prop_tr'
+    |> show_types ? (#1 o prune_typs o rpair [])
+    |> mark_atoms
+    |> ast_of
+  end;
+
+
+
 (** unparse **)
 
+(** unparse terms, typs, sorts **)
+
+local
+
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+
+fun unparse_t t_to_ast prt_t markup ctxt curried t =
+  let
+    val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
+      Syntax.rep_syntax (ProofContext.syn_of ctxt);
+    val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
+  in
+    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
+      (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
+      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
+  end;
+
+in
+
+fun standard_unparse_sort {extern_class} ctxt =
+  unparse_t (K sort_to_ast)
+    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+    Markup.sort ctxt false;
+
+fun standard_unparse_typ extern ctxt =
+  unparse_t (K typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt false;
+
+fun standard_unparse_term idents extern =
+  unparse_t (term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
+
+end;
+
+
 fun unparse_sort ctxt =
-  Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
-    ctxt (ProofContext.syn_of ctxt);
+  standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} ctxt;
 
 fun unparse_typ ctxt =
   let
     val tsig = ProofContext.tsig_of ctxt;
     val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
-  in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
+  in standard_unparse_typ extern ctxt end;
 
 fun unparse_term ctxt =
   let
@@ -412,11 +610,47 @@
       extern_type = Type.extern_type tsig,
       extern_const = Consts.extern consts};
   in
-    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
-      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
+    standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+      (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
   end;
 
 
+
+(** translations **)
+
+(* type propositions *)
+
+fun type_prop_tr' _ T [Const ("\\<^const>Pure.sort_constraint", _)] =
+      Lexicon.const "_sort_constraint" $ term_of_typ true T
+  | type_prop_tr' show_sorts T [t] =
+      Lexicon.const "_ofclass" $ term_of_typ show_sorts T $ t
+  | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
+
+
+(* type reflection *)
+
+fun type_tr' show_sorts (Type ("itself", [T])) ts =
+      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ show_sorts T, ts)
+  | type_tr' _ _ _ = raise Match;
+
+
+(* type constraints *)
+
+fun type_constraint_tr' show_sorts (Type ("fun", [T, _])) (t :: ts) =
+      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ show_sorts T, ts)
+  | type_constraint_tr' _ _ _ = raise Match;
+
+
+(* setup translations *)
+
+val _ = Context.>> (Context.map_theory
+  (Sign.add_trfunsT
+   [("_type_prop", type_prop_tr'),
+    ("\\<^const>TYPE", type_tr'),
+    ("_type_constraint_", type_constraint_tr')]));
+
+
+
 (** install operations **)
 
 val _ = Syntax.install_operations
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -10,7 +10,6 @@
   val is_position: term -> bool
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
-  val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
 end;
@@ -18,7 +17,6 @@
 signature TYPE_EXT =
 sig
   include TYPE_EXT0
-  val term_of_sort: sort -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val type_ext: Syn_Ext.syn_ext
 end;
@@ -52,42 +50,6 @@
 
 
 
-(** output utils **)
-
-(* term_of_sort *)
-
-fun term_of_sort S =
-  let
-    val class = Lexicon.const o Lexicon.mark_class;
-
-    fun classes [c] = class c
-      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
-  in
-    (case S of
-      [] => Lexicon.const "_topsort"
-    | [c] => class c
-    | cs => Lexicon.const "_sort" $ classes cs)
-  end;
-
-
-(* term_of_typ *)
-
-fun term_of_typ show_sorts ty =
-  let
-    fun of_sort t S =
-      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
-      else t;
-
-    fun term_of (Type (a, Ts)) =
-          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
-      | term_of (TFree (x, S)) =
-          if is_some (Lexicon.decode_position x) then Lexicon.free x
-          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
-      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
-  in term_of ty end;
-
-
-
 (** the type syntax **)
 
 (* print mode *)
diff -r 15bba1fb39d1 -r 29e3967550d5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/Pure/pure_thy.ML	Wed Apr 06 12:58:13 2011 +0200
@@ -146,7 +146,6 @@
   #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
   #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   #> Sign.add_trfuns Syntax.pure_trfuns
-  #> Sign.add_trfunsT Syntax.pure_trfunsT
   #> Sign.local_path
   #> Sign.add_consts_i
    [(Binding.name "term", typ "'a => prop", NoSyn),