typed_print_translation: discontinued show_sorts argument;

--- a/NEWS	Wed Apr 06 13:27:59 2011 +0200
+++ b/NEWS	Wed Apr 06 13:33:46 2011 +0200
@@ -97,6 +97,9 @@
 content, no inclusion in structure Syntax.  INCOMPATIBILITY, refer to
 qualified names like Ast.Constant etc.
 
+* Typed print translation: discontinued show_sorts argument, which is
+already available via context of "advanced" translation.
+
 
 
 New in Isabelle2011 (January 2011)

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -804,8 +804,7 @@
 val parse_ast_translation   : (string * (ast list -> ast)) list
 val parse_translation       : (string * (term list -> term)) list
 val print_translation       : (string * (term list -> term)) list
-val typed_print_translation :
-  (string * (bool -> typ -> term list -> term)) list
+val typed_print_translation : (string * (typ -> term list -> term)) list
 val print_ast_translation   : (string * (ast list -> ast)) list
 \end{ttbox}
 
@@ -827,7 +826,7 @@
 val print_translation:
   (string * (Proof.context -> term list -> term)) list
 val typed_print_translation:
-  (string * (Proof.context -> bool -> typ -> term list -> term)) list
+  (string * (Proof.context -> typ -> term list -> term)) list
 val print_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
 \end{ttbox}

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:27:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:33:46 2011 +0200
@@ -824,8 +824,7 @@
 val parse_ast_translation   : (string * (ast list -> ast)) list
 val parse_translation       : (string * (term list -> term)) list
 val print_translation       : (string * (term list -> term)) list
-val typed_print_translation :
-  (string * (bool -> typ -> term list -> term)) list
+val typed_print_translation : (string * (typ -> term list -> term)) list
 val print_ast_translation   : (string * (ast list -> ast)) list
 \end{ttbox}
 
@@ -847,7 +846,7 @@
 val print_translation:
   (string * (Proof.context -> term list -> term)) list
 val typed_print_translation:
-  (string * (Proof.context -> bool -> typ -> term list -> term)) list
+  (string * (Proof.context -> typ -> term list -> term)) list
 val print_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
 \end{ttbox}%

--- a/src/HOL/Groups.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Groups.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -125,13 +125,13 @@
 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
 
 typed_print_translation (advanced) {*
-let
-  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
-    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_Phases.term_of_typ show_sorts T);
-in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
+  let
+    fun tr' c = (c, fn ctxt => fn T => fn ts =>
+      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_Phases.term_of_typ ctxt T);
+  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
 *} -- {* show types that are presumably too general *}
 
 class plus =

--- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -34,12 +34,11 @@
 
 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
 
-typed_print_translation {*
-let
-  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
-    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
-in [(@{const_syntax card}, card_univ_tr')]
-end
+typed_print_translation (advanced) {*
+  let
+    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
+      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
+  in [(@{const_syntax card}, card_univ_tr')] end
 *}
 
 lemma card_unit [simp]: "CARD(unit) = 1"

--- a/src/HOL/Product_Type.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -232,8 +232,8 @@
 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
 typed_print_translation {*
 let
-  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
-    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
+  fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+    | split_guess_names_tr' T [Abs (x, xT, t)] =
         (case (head_of t) of
           Const (@{const_syntax prod_case}, _) => raise Match
         | _ =>
@@ -245,7 +245,7 @@
             Syntax.const @{syntax_const "_abs"} $
               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
           end)
-    | split_guess_names_tr' _ T [t] =
+    | split_guess_names_tr' T [t] =
         (case head_of t of
           Const (@{const_syntax prod_case}, _) => raise Match
         | _ =>
@@ -257,7 +257,7 @@
             Syntax.const @{syntax_const "_abs"} $
               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
           end)
-    | split_guess_names_tr' _ _ _ = raise Match;
+    | split_guess_names_tr' _ _ = raise Match;
 in [(@{const_syntax prod_case}, split_guess_names_tr')] end
 *}
 

--- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -69,17 +69,17 @@
 
 in
 
-fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
+fun numeral_tr' ctxt (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_Phases.term_of_typ show_sorts T
+            Syntax_Phases.term_of_typ ctxt T
       in list_comb (t', ts) end
-  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
+  | numeral_tr' _ T (t :: ts) =
       if T = dummyT then list_comb (syntax_numeral t, ts)
       else raise Match
-  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
+  | numeral_tr' _ _ _ = raise Match;
 
 end;
 

--- a/src/HOL/Tools/record.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Tools/record.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -708,9 +708,9 @@
 
                     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_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));
+                      map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
+                        (#1 (split_last alphas));
 
                     val more' = mk_ext rest;
                   in
@@ -819,8 +819,6 @@
     val T = decode_type thy t;
     val varifyT = varifyT (Term.maxidx_of_typ T);
 
-    val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
-
     fun strip_fields T =
       (case T of
         Type (ext, args as _ :: _) =>
@@ -847,11 +845,15 @@
 
     val (fields, (_, moreT)) = split_last (strip_fields T);
     val _ = null fields andalso raise Match;
-    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
+    val u =
+      foldr1 field_types_tr'
+        (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
   in
     if not (! print_type_as_fields) orelse null fields then raise Match
     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
-    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
+    else
+      Syntax.const @{syntax_const "_record_type_scheme"} $ u $
+        Syntax_Phases.term_of_typ ctxt moreT
   end;
 
 (*try to reconstruct the record name type abbreviation from
@@ -865,7 +867,7 @@
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
-      in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
+      in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in

--- a/src/HOL/Typerep.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/Typerep.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -30,13 +30,13 @@
 in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
 *}
 
-typed_print_translation {*
+typed_print_translation (advanced) {*
 let
-  fun typerep_tr' show_sorts (*"typerep"*)
+  fun typerep_tr' ctxt (*"typerep"*)
           (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
           (Const (@{const_syntax TYPE}, _) :: ts) =
         Term.list_comb
-          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
+          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
     | typerep_tr' _ T ts = raise Match;
 in [(@{const_syntax typerep}, typerep_tr')] end
 *}

--- a/src/HOL/ex/Numeral.thy	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 13:33:46 2011 +0200
@@ -301,7 +301,7 @@
     | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
         dig 1 (int_of_num' n)
     | int_of_num' (Const (@{const_syntax One}, _)) = 1;
-  fun num_tr' ctxt show_sorts T [n] =
+  fun num_tr' ctxt T [n] =
     let
       val k = int_of_num' n;
       val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
@@ -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_Phases.term_of_typ show_sorts T'
+          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ ctxt T'
       | T' => if T' = dummyT then t' else raise Match
     end;
 in [(@{const_syntax of_num}, num_tr')] end

--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -148,8 +148,7 @@
 fun typed_print_translation (a, (txt, pos)) =
   ML_Lex.read pos txt
   |> ML_Context.expression pos
-    ("val typed_print_translation: (string * (" ^ advancedT a ^
-      "bool -> typ -> term list -> term)) list")
+    ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   |> Context.theory_map;
 

--- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -50,8 +50,7 @@
       parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
       parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
-      print_translation:
-        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
+      print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
@@ -60,14 +59,14 @@
   val syn_ext': bool -> (string -> bool) -> mfix list ->
     string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (Proof.context -> string -> Pretty.T)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (Proof.context -> string -> Pretty.T)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
@@ -76,12 +75,12 @@
   val syn_ext_trfuns:
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
-    (string * ((bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((typ -> term list -> term) * stamp)) list *
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_advanced_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> 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 pure_ext: syn_ext
@@ -337,8 +336,7 @@
     parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
     parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
-    print_translation:
-      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
+    print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
     print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};

--- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -33,8 +33,8 @@
 signature SYN_TRANS1 =
 sig
   include SYN_TRANS0
-  val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
-  val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
+  val non_typed_tr': (term list -> term) -> typ -> term list -> term
+  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
   val constrainAbsC: string
   val abs_tr: term list -> term
   val pure_trfuns:
@@ -45,7 +45,7 @@
   val struct_trfuns: string list ->
     (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
-    (string * (bool -> typ -> term list -> term)) list *
+    (string * (typ -> term list -> term)) list *
     (string * (Ast.ast list -> Ast.ast)) list
 end;
 
@@ -243,8 +243,8 @@
 
 (* types *)
 
-fun non_typed_tr' f _ _ ts = f ts;
-fun non_typed_tr'' f x _ _ ts = f x ts;
+fun non_typed_tr' f _ ts = f ts;
+fun non_typed_tr'' f x _ ts = f x ts;
 
 
 (* application *)

--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -109,7 +109,7 @@
     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
     parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
-    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+    print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
@@ -141,12 +141,12 @@
   val update_trfuns:
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
-    (string * ((bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((typ -> term list -> term) * stamp)) list *
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val update_advanced_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
-    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
     syntax -> syntax
@@ -480,7 +480,7 @@
     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
     parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
-    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+    print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -12,7 +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
+  val term_of_typ: Proof.context -> typ -> term
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
@@ -411,8 +411,10 @@
 
 (* term_of_typ *)
 
-fun term_of_typ show_sorts ty =
+fun term_of_typ ctxt ty =
   let
+    val show_sorts = Config.get ctxt show_sorts;
+
     fun of_sort t S =
       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
       else t;
@@ -444,7 +446,7 @@
 
 (* 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 apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs;
 
 fun ast_of_termT ctxt trf tm =
   let
@@ -463,7 +465,7 @@
   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);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
 
 
 (* term_to_ast *)
@@ -544,7 +546,7 @@
     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)]
+          ast_of_termT ctxt trf (term_of_typ ctxt T)]
       else simple_ast_of ctxt t;
   in
     tm
@@ -620,31 +622,31 @@
 
 (* 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
+fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
+      Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
+  | type_prop_tr' ctxt T [t] =
+      Lexicon.const "_ofclass" $ term_of_typ ctxt 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)
+fun type_tr' ctxt (Type ("itself", [T])) ts =
+      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt 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)
+fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
+      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
   | type_constraint_tr' _ _ _ = raise Match;
 
 
 (* setup translations *)
 
 val _ = Context.>> (Context.map_theory
-  (Sign.add_trfunsT
+  (Sign.add_advanced_trfunsT
    [("_type_prop", type_prop_tr'),
     ("\\<^const>TYPE", type_tr'),
     ("_type_constraint_", type_constraint_tr')]));

--- a/src/Pure/sign.ML	Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/sign.ML	Wed Apr 06 13:33:46 2011 +0200
@@ -95,15 +95,14 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
-  val add_trfunsT:
-    (string * (bool -> typ -> term list -> term)) list -> theory -> theory
+  val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
   val add_advanced_trfuns:
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
     (string * (Proof.context -> term list -> term)) list *
     (string * (Proof.context -> term list -> term)) list *
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_advanced_trfunsT:
-    (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
+    (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
     (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list