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

     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Apr 06 13:27:59 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Apr 06 13:33:46 2011 +0200
     2.3 @@ -804,8 +804,7 @@
     2.4  val parse_ast_translation   : (string * (ast list -> ast)) list
     2.5  val parse_translation       : (string * (term list -> term)) list
     2.6  val print_translation       : (string * (term list -> term)) list
     2.7 -val typed_print_translation :
     2.8 -  (string * (bool -> typ -> term list -> term)) list
     2.9 +val typed_print_translation : (string * (typ -> term list -> term)) list
    2.10  val print_ast_translation   : (string * (ast list -> ast)) list
    2.11  \end{ttbox}
    2.12  
    2.13 @@ -827,7 +826,7 @@
    2.14  val print_translation:
    2.15    (string * (Proof.context -> term list -> term)) list
    2.16  val typed_print_translation:
    2.17 -  (string * (Proof.context -> bool -> typ -> term list -> term)) list
    2.18 +  (string * (Proof.context -> typ -> term list -> term)) list
    2.19  val print_ast_translation:
    2.20    (string * (Proof.context -> ast list -> ast)) list
    2.21  \end{ttbox}

     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:27:59 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:33:46 2011 +0200
     3.3 @@ -824,8 +824,7 @@
     3.4  val parse_ast_translation   : (string * (ast list -> ast)) list
     3.5  val parse_translation       : (string * (term list -> term)) list
     3.6  val print_translation       : (string * (term list -> term)) list
     3.7 -val typed_print_translation :
     3.8 -  (string * (bool -> typ -> term list -> term)) list
     3.9 +val typed_print_translation : (string * (typ -> term list -> term)) list
    3.10  val print_ast_translation   : (string * (ast list -> ast)) list
    3.11  \end{ttbox}
    3.12  
    3.13 @@ -847,7 +846,7 @@
    3.14  val print_translation:
    3.15    (string * (Proof.context -> term list -> term)) list
    3.16  val typed_print_translation:
    3.17 -  (string * (Proof.context -> bool -> typ -> term list -> term)) list
    3.18 +  (string * (Proof.context -> typ -> term list -> term)) list
    3.19  val print_ast_translation:
    3.20    (string * (Proof.context -> ast list -> ast)) list
    3.21  \end{ttbox}%

     4.1 --- a/src/HOL/Groups.thy	Wed Apr 06 13:27:59 2011 +0200
     4.2 +++ b/src/HOL/Groups.thy	Wed Apr 06 13:33:46 2011 +0200
     4.3 @@ -125,13 +125,13 @@
     4.4  simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
     4.5  
     4.6  typed_print_translation (advanced) {*
     4.7 -let
     4.8 -  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
     4.9 -    if not (null ts) orelse T = dummyT
    4.10 -      orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    4.11 -    then raise Match
    4.12 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T);
    4.13 -in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    4.14 +  let
    4.15 +    fun tr' c = (c, fn ctxt => fn T => fn ts =>
    4.16 +      if not (null ts) orelse T = dummyT
    4.17 +        orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    4.18 +      then raise Match
    4.19 +      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T);
    4.20 +  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    4.21  *} -- {* show types that are presumably too general *}
    4.22  
    4.23  class plus =

     5.1 --- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:27:59 2011 +0200
     5.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:33:46 2011 +0200
     5.3 @@ -34,12 +34,11 @@
     5.4  
     5.5  translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
     5.6  
     5.7 -typed_print_translation {*
     5.8 -let
     5.9 -  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
    5.10 -    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
    5.11 -in [(@{const_syntax card}, card_univ_tr')]
    5.12 -end
    5.13 +typed_print_translation (advanced) {*
    5.14 +  let
    5.15 +    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
    5.16 +      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
    5.17 +  in [(@{const_syntax card}, card_univ_tr')] end
    5.18  *}
    5.19  
    5.20  lemma card_unit [simp]: "CARD(unit) = 1"

     6.1 --- a/src/HOL/Product_Type.thy	Wed Apr 06 13:27:59 2011 +0200
     6.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 06 13:33:46 2011 +0200
     6.3 @@ -232,8 +232,8 @@
     6.4  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
     6.5  typed_print_translation {*
     6.6  let
     6.7 -  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
     6.8 -    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
     6.9 +  fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
    6.10 +    | split_guess_names_tr' T [Abs (x, xT, t)] =
    6.11          (case (head_of t) of
    6.12            Const (@{const_syntax prod_case}, _) => raise Match
    6.13          | _ =>
    6.14 @@ -245,7 +245,7 @@
    6.15              Syntax.const @{syntax_const "_abs"} $
    6.16                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    6.17            end)
    6.18 -    | split_guess_names_tr' _ T [t] =
    6.19 +    | split_guess_names_tr' T [t] =
    6.20          (case head_of t of
    6.21            Const (@{const_syntax prod_case}, _) => raise Match
    6.22          | _ =>
    6.23 @@ -257,7 +257,7 @@
    6.24              Syntax.const @{syntax_const "_abs"} $
    6.25                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    6.26            end)
    6.27 -    | split_guess_names_tr' _ _ _ = raise Match;
    6.28 +    | split_guess_names_tr' _ _ = raise Match;
    6.29  in [(@{const_syntax prod_case}, split_guess_names_tr')] end
    6.30  *}
    6.31  

     7.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:27:59 2011 +0200
     7.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
     7.3 @@ -69,17 +69,17 @@
     7.4  
     7.5  in
     7.6  
     7.7 -fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
     7.8 +fun numeral_tr' ctxt (Type (@{type_name fun}, [_, T])) (t :: ts) =
     7.9        let val t' =
    7.10          if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
    7.11          else
    7.12            Syntax.const Syntax.constrainC $ syntax_numeral t $
    7.13 -            Syntax_Phases.term_of_typ show_sorts T
    7.14 +            Syntax_Phases.term_of_typ ctxt T
    7.15        in list_comb (t', ts) end
    7.16 -  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
    7.17 +  | numeral_tr' _ T (t :: ts) =
    7.18        if T = dummyT then list_comb (syntax_numeral t, ts)
    7.19        else raise Match
    7.20 -  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
    7.21 +  | numeral_tr' _ _ _ = raise Match;
    7.22  
    7.23  end;
    7.24  

     8.1 --- a/src/HOL/Tools/record.ML	Wed Apr 06 13:27:59 2011 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Wed Apr 06 13:33:46 2011 +0200
     8.3 @@ -708,9 +708,9 @@
     8.4  
     8.5                      val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
     8.6                        handle Type.TYPE_MATCH => err "type is no proper record (extension)";
     8.7 -                    val term_of_typ = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
     8.8                      val alphas' =
     8.9 -                      map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
    8.10 +                      map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
    8.11 +                        (#1 (split_last alphas));
    8.12  
    8.13                      val more' = mk_ext rest;
    8.14                    in
    8.15 @@ -819,8 +819,6 @@
    8.16      val T = decode_type thy t;
    8.17      val varifyT = varifyT (Term.maxidx_of_typ T);
    8.18  
    8.19 -    val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
    8.20 -
    8.21      fun strip_fields T =
    8.22        (case T of
    8.23          Type (ext, args as _ :: _) =>
    8.24 @@ -847,11 +845,15 @@
    8.25  
    8.26      val (fields, (_, moreT)) = split_last (strip_fields T);
    8.27      val _ = null fields andalso raise Match;
    8.28 -    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
    8.29 +    val u =
    8.30 +      foldr1 field_types_tr'
    8.31 +        (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
    8.32    in
    8.33      if not (! print_type_as_fields) orelse null fields then raise Match
    8.34      else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
    8.35 -    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
    8.36 +    else
    8.37 +      Syntax.const @{syntax_const "_record_type_scheme"} $ u $
    8.38 +        Syntax_Phases.term_of_typ ctxt moreT
    8.39    end;
    8.40  
    8.41  (*try to reconstruct the record name type abbreviation from
    8.42 @@ -865,7 +867,7 @@
    8.43  
    8.44      fun mk_type_abbr subst name args =
    8.45        let val abbrT = Type (name, map (varifyT o TFree) args)
    8.46 -      in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
    8.47 +      in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
    8.48  
    8.49      fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
    8.50    in

     9.1 --- a/src/HOL/Typerep.thy	Wed Apr 06 13:27:59 2011 +0200
     9.2 +++ b/src/HOL/Typerep.thy	Wed Apr 06 13:33:46 2011 +0200
     9.3 @@ -30,13 +30,13 @@
     9.4  in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
     9.5  *}
     9.6  
     9.7 -typed_print_translation {*
     9.8 +typed_print_translation (advanced) {*
     9.9  let
    9.10 -  fun typerep_tr' show_sorts (*"typerep"*)
    9.11 +  fun typerep_tr' ctxt (*"typerep"*)
    9.12            (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
    9.13            (Const (@{const_syntax TYPE}, _) :: ts) =
    9.14          Term.list_comb
    9.15 -          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
    9.16 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    9.17      | typerep_tr' _ T ts = raise Match;
    9.18  in [(@{const_syntax typerep}, typerep_tr')] end
    9.19  *}

    10.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 06 13:27:59 2011 +0200
    10.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 06 13:33:46 2011 +0200
    10.3 @@ -301,7 +301,7 @@
    10.4      | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
    10.5          dig 1 (int_of_num' n)
    10.6      | int_of_num' (Const (@{const_syntax One}, _)) = 1;
    10.7 -  fun num_tr' ctxt show_sorts T [n] =
    10.8 +  fun num_tr' ctxt T [n] =
    10.9      let
   10.10        val k = int_of_num' n;
   10.11        val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
   10.12 @@ -309,7 +309,7 @@
   10.13        case T of
   10.14          Type (@{type_name fun}, [_, T']) =>
   10.15            if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
   10.16 -          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ show_sorts T'
   10.17 +          else Syntax.const Syntax.constrainC $ t' $ Syntax_Phases.term_of_typ ctxt T'
   10.18        | T' => if T' = dummyT then t' else raise Match
   10.19      end;
   10.20  in [(@{const_syntax of_num}, num_tr')] end

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

    12.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:27:59 2011 +0200
    12.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Apr 06 13:33:46 2011 +0200
    12.3 @@ -50,8 +50,7 @@
    12.4        parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    12.5        parse_rules: (Ast.ast * Ast.ast) list,
    12.6        parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    12.7 -      print_translation:
    12.8 -        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    12.9 +      print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   12.10        print_rules: (Ast.ast * Ast.ast) list,
   12.11        print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   12.12        token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
   12.13 @@ -60,14 +59,14 @@
   12.14    val syn_ext': bool -> (string -> bool) -> mfix list ->
   12.15      string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   12.16      (string * ((Proof.context -> term list -> term) * stamp)) list *
   12.17 -    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   12.18 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   12.19      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
   12.20      -> (string * string * (Proof.context -> string -> Pretty.T)) list
   12.21      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   12.22    val syn_ext: mfix list -> string list ->
   12.23      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   12.24      (string * ((Proof.context -> term list -> term) * stamp)) list *
   12.25 -    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   12.26 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   12.27      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
   12.28      -> (string * string * (Proof.context -> string -> Pretty.T)) list
   12.29      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   12.30 @@ -76,12 +75,12 @@
   12.31    val syn_ext_trfuns:
   12.32      (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   12.33      (string * ((term list -> term) * stamp)) list *
   12.34 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
   12.35 +    (string * ((typ -> term list -> term) * stamp)) list *
   12.36      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   12.37    val syn_ext_advanced_trfuns:
   12.38      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   12.39      (string * ((Proof.context -> term list -> term) * stamp)) list *
   12.40 -    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   12.41 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   12.42      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   12.43    val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
   12.44    val pure_ext: syn_ext
   12.45 @@ -337,8 +336,7 @@
   12.46      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   12.47      parse_rules: (Ast.ast * Ast.ast) list,
   12.48      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
   12.49 -    print_translation:
   12.50 -      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
   12.51 +    print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   12.52      print_rules: (Ast.ast * Ast.ast) list,
   12.53      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   12.54      token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};

    13.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 13:27:59 2011 +0200
    13.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Apr 06 13:33:46 2011 +0200
    13.3 @@ -33,8 +33,8 @@
    13.4  signature SYN_TRANS1 =
    13.5  sig
    13.6    include SYN_TRANS0
    13.7 -  val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
    13.8 -  val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
    13.9 +  val non_typed_tr': (term list -> term) -> typ -> term list -> term
   13.10 +  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
   13.11    val constrainAbsC: string
   13.12    val abs_tr: term list -> term
   13.13    val pure_trfuns:
   13.14 @@ -45,7 +45,7 @@
   13.15    val struct_trfuns: string list ->
   13.16      (string * (Ast.ast list -> Ast.ast)) list *
   13.17      (string * (term list -> term)) list *
   13.18 -    (string * (bool -> typ -> term list -> term)) list *
   13.19 +    (string * (typ -> term list -> term)) list *
   13.20      (string * (Ast.ast list -> Ast.ast)) list
   13.21  end;
   13.22  
   13.23 @@ -243,8 +243,8 @@
   13.24  
   13.25  (* types *)
   13.26  
   13.27 -fun non_typed_tr' f _ _ ts = f ts;
   13.28 -fun non_typed_tr'' f x _ _ ts = f x ts;
   13.29 +fun non_typed_tr' f _ ts = f ts;
   13.30 +fun non_typed_tr'' f x _ ts = f x ts;
   13.31  
   13.32  
   13.33  (* application *)

    14.1 --- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 13:27:59 2011 +0200
    14.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 13:33:46 2011 +0200
    14.3 @@ -109,7 +109,7 @@
    14.4      parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    14.5      parse_ruletab: ruletab,
    14.6      parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
    14.7 -    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    14.8 +    print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
    14.9      print_ruletab: ruletab,
   14.10      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
   14.11      tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
   14.12 @@ -141,12 +141,12 @@
   14.13    val update_trfuns:
   14.14      (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   14.15      (string * ((term list -> term) * stamp)) list *
   14.16 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
   14.17 +    (string * ((typ -> term list -> term) * stamp)) list *
   14.18      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   14.19    val update_advanced_trfuns:
   14.20      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   14.21      (string * ((Proof.context -> term list -> term) * stamp)) list *
   14.22 -    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   14.23 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   14.24      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   14.25    val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
   14.26      syntax -> syntax
   14.27 @@ -480,7 +480,7 @@
   14.28      parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
   14.29      parse_ruletab: ruletab,
   14.30      parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
   14.31 -    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
   14.32 +    print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
   14.33      print_ruletab: ruletab,
   14.34      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
   14.35      tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,

    15.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:27:59 2011 +0200
    15.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 13:33:46 2011 +0200
    15.3 @@ -12,7 +12,7 @@
    15.4    val decode_term: Proof.context ->
    15.5      Position.reports * term Exn.result -> Position.reports * term Exn.result
    15.6    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    15.7 -  val term_of_typ: bool -> typ -> term
    15.8 +  val term_of_typ: Proof.context -> typ -> term
    15.9  end
   15.10  
   15.11  structure Syntax_Phases: SYNTAX_PHASES =
   15.12 @@ -411,8 +411,10 @@
   15.13  
   15.14  (* term_of_typ *)
   15.15  
   15.16 -fun term_of_typ show_sorts ty =
   15.17 +fun term_of_typ ctxt ty =
   15.18    let
   15.19 +    val show_sorts = Config.get ctxt show_sorts;
   15.20 +
   15.21      fun of_sort t S =
   15.22        if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   15.23        else t;
   15.24 @@ -444,7 +446,7 @@
   15.25  
   15.26  (* sort_to_ast and typ_to_ast *)
   15.27  
   15.28 -fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
   15.29 +fun apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs;
   15.30  
   15.31  fun ast_of_termT ctxt trf tm =
   15.32    let
   15.33 @@ -463,7 +465,7 @@
   15.34    in ast_of tm end;
   15.35  
   15.36  fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
   15.37 -fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ (Config.get ctxt show_sorts) T);
   15.38 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
   15.39  
   15.40  
   15.41  (* term_to_ast *)
   15.42 @@ -544,7 +546,7 @@
   15.43      and constrain t T =
   15.44        if show_types andalso T <> dummyT then
   15.45          Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
   15.46 -          ast_of_termT ctxt trf (term_of_typ show_sorts T)]
   15.47 +          ast_of_termT ctxt trf (term_of_typ ctxt T)]
   15.48        else simple_ast_of ctxt t;
   15.49    in
   15.50      tm
   15.51 @@ -620,31 +622,31 @@
   15.52  
   15.53  (* type propositions *)
   15.54  
   15.55 -fun type_prop_tr' _ T [Const ("\\<^const>Pure.sort_constraint", _)] =
   15.56 -      Lexicon.const "_sort_constraint" $ term_of_typ true T
   15.57 -  | type_prop_tr' show_sorts T [t] =
   15.58 -      Lexicon.const "_ofclass" $ term_of_typ show_sorts T $ t
   15.59 +fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
   15.60 +      Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   15.61 +  | type_prop_tr' ctxt T [t] =
   15.62 +      Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
   15.63    | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
   15.64  
   15.65  
   15.66  (* type reflection *)
   15.67  
   15.68 -fun type_tr' show_sorts (Type ("itself", [T])) ts =
   15.69 -      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ show_sorts T, ts)
   15.70 +fun type_tr' ctxt (Type ("itself", [T])) ts =
   15.71 +      Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
   15.72    | type_tr' _ _ _ = raise Match;
   15.73  
   15.74  
   15.75  (* type constraints *)
   15.76  
   15.77 -fun type_constraint_tr' show_sorts (Type ("fun", [T, _])) (t :: ts) =
   15.78 -      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ show_sorts T, ts)
   15.79 +fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
   15.80 +      Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
   15.81    | type_constraint_tr' _ _ _ = raise Match;
   15.82  
   15.83  
   15.84  (* setup translations *)
   15.85  
   15.86  val _ = Context.>> (Context.map_theory
   15.87 -  (Sign.add_trfunsT
   15.88 +  (Sign.add_advanced_trfunsT
   15.89     [("_type_prop", type_prop_tr'),
   15.90      ("\\<^const>TYPE", type_tr'),
   15.91      ("_type_constraint_", type_constraint_tr')]));

    16.1 --- a/src/Pure/sign.ML	Wed Apr 06 13:27:59 2011 +0200
    16.2 +++ b/src/Pure/sign.ML	Wed Apr 06 13:33:46 2011 +0200
    16.3 @@ -95,15 +95,14 @@
    16.4      (string * (term list -> term)) list *
    16.5      (string * (term list -> term)) list *
    16.6      (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
    16.7 -  val add_trfunsT:
    16.8 -    (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    16.9 +  val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
   16.10    val add_advanced_trfuns:
   16.11      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
   16.12      (string * (Proof.context -> term list -> term)) list *
   16.13      (string * (Proof.context -> term list -> term)) list *
   16.14      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   16.15    val add_advanced_trfunsT:
   16.16 -    (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   16.17 +    (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
   16.18    val add_tokentrfuns:
   16.19      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
   16.20    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list