merged
authorwenzelm
Sat May 25 18:30:38 2013 +0200 (2013-05-25)
changeset 52148893b15200ec1
parent 52141 eff000cab70f
parent 52147 9943f8067f11
child 52149 32b1dbda331c
merged
NEWS
src/HOL/List.thy
src/HOL/Tools/float_syntax.ML
src/Pure/Isar/expression.ML
     1.1 --- a/NEWS	Sat May 25 15:44:29 2013 +0200
     1.2 +++ b/NEWS	Sat May 25 18:30:38 2013 +0200
     1.3 @@ -40,6 +40,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Syntax translation functions (print_translation etc.) always depend
     1.8 +on Proof.context.  Discontinued former "(advanced)" option -- this is
     1.9 +now the default.  Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Target-sensitive commands 'interpretation' and 'sublocale'.
    1.12  Particulary, 'interpretation' now allows for non-persistent
    1.13  interpretation within "context ... begin ... end" blocks.
     2.1 --- a/etc/isar-keywords-ZF.el	Sat May 25 15:44:29 2013 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Sat May 25 18:30:38 2013 +0200
     2.3 @@ -209,8 +209,7 @@
     2.4      "}"))
     2.5  
     2.6  (defconst isar-keywords-minor
     2.7 -  '("advanced"
     2.8 -    "and"
     2.9 +  '("and"
    2.10      "assumes"
    2.11      "attach"
    2.12      "begin"
     3.1 --- a/etc/isar-keywords.el	Sat May 25 15:44:29 2013 +0200
     3.2 +++ b/etc/isar-keywords.el	Sat May 25 18:30:38 2013 +0200
     3.3 @@ -52,11 +52,13 @@
     3.4      "code_const"
     3.5      "code_datatype"
     3.6      "code_deps"
     3.7 +    "code_identifier"
     3.8      "code_include"
     3.9      "code_instance"
    3.10      "code_modulename"
    3.11      "code_monad"
    3.12      "code_pred"
    3.13 +    "code_printing"
    3.14      "code_reflect"
    3.15      "code_reserved"
    3.16      "code_thms"
    3.17 @@ -301,15 +303,18 @@
    3.18      "}"))
    3.19  
    3.20  (defconst isar-keywords-minor
    3.21 -  '("advanced"
    3.22 -    "and"
    3.23 +  '("and"
    3.24      "assumes"
    3.25      "attach"
    3.26      "avoids"
    3.27      "begin"
    3.28      "binder"
    3.29      "checking"
    3.30 +    "class_instance"
    3.31 +    "class_relation"
    3.32 +    "code_module"
    3.33      "congs"
    3.34 +    "constant"
    3.35      "constrains"
    3.36      "datatypes"
    3.37      "defaults"
    3.38 @@ -345,6 +350,8 @@
    3.39      "rep_compat"
    3.40      "shows"
    3.41      "structure"
    3.42 +    "type_class"
    3.43 +    "type_constructor"
    3.44      "unchecked"
    3.45      "unsafe"
    3.46      "where"))
    3.47 @@ -487,10 +494,12 @@
    3.48      "code_class"
    3.49      "code_const"
    3.50      "code_datatype"
    3.51 +    "code_identifier"
    3.52      "code_include"
    3.53      "code_instance"
    3.54      "code_modulename"
    3.55      "code_monad"
    3.56 +    "code_printing"
    3.57      "code_reflect"
    3.58      "code_reserved"
    3.59      "code_type"
     4.1 --- a/src/CCL/Term.thy	Sat May 25 15:44:29 2013 +0200
     4.2 +++ b/src/CCL/Term.thy	Sat May 25 18:30:38 2013 +0200
     4.3 @@ -95,17 +95,17 @@
     4.4  *}
     4.5  
     4.6  parse_translation {*
     4.7 - [(@{syntax_const "_let"}, let_tr),
     4.8 -  (@{syntax_const "_letrec"}, letrec_tr),
     4.9 -  (@{syntax_const "_letrec2"}, letrec2_tr),
    4.10 -  (@{syntax_const "_letrec3"}, letrec3_tr)]
    4.11 + [(@{syntax_const "_let"}, K let_tr),
    4.12 +  (@{syntax_const "_letrec"}, K letrec_tr),
    4.13 +  (@{syntax_const "_letrec2"}, K letrec2_tr),
    4.14 +  (@{syntax_const "_letrec3"}, K letrec3_tr)]
    4.15  *}
    4.16  
    4.17  print_translation {*
    4.18 - [(@{const_syntax let}, let_tr'),
    4.19 -  (@{const_syntax letrec}, letrec_tr'),
    4.20 -  (@{const_syntax letrec2}, letrec2_tr'),
    4.21 -  (@{const_syntax letrec3}, letrec3_tr')]
    4.22 + [(@{const_syntax let}, K let_tr'),
    4.23 +  (@{const_syntax letrec}, K letrec_tr'),
    4.24 +  (@{const_syntax letrec2}, K letrec2_tr'),
    4.25 +  (@{const_syntax letrec3}, K letrec3_tr')]
    4.26  *}
    4.27  
    4.28  consts
     5.1 --- a/src/CCL/Type.thy	Sat May 25 15:44:29 2013 +0200
     5.2 +++ b/src/CCL/Type.thy	Sat May 25 18:30:38 2013 +0200
     5.3 @@ -47,9 +47,9 @@
     5.4  
     5.5  print_translation {*
     5.6   [(@{const_syntax Pi},
     5.7 -    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
     5.8 +    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
     5.9    (@{const_syntax Sigma},
    5.10 -    Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
    5.11 +    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
    5.12  *}
    5.13  
    5.14  defs
     6.1 --- a/src/Cube/Cube.thy	Sat May 25 15:44:29 2013 +0200
     6.2 +++ b/src/Cube/Cube.thy	Sat May 25 18:30:38 2013 +0200
     6.3 @@ -63,7 +63,7 @@
     6.4  
     6.5  print_translation {*
     6.6    [(@{const_syntax Prod},
     6.7 -    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
     6.8 +    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
     6.9  *}
    6.10  
    6.11  axiomatization where
     7.1 --- a/src/Doc/Classes/Setup.thy	Sat May 25 15:44:29 2013 +0200
     7.2 +++ b/src/Doc/Classes/Setup.thy	Sat May 25 18:30:38 2013 +0200
     7.3 @@ -30,10 +30,10 @@
     7.4            Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
     7.5        | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
     7.6    in
     7.7 -   [(@{syntax_const "_alpha"}, alpha_ast_tr),
     7.8 -    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
     7.9 -    (@{syntax_const "_beta"}, beta_ast_tr),
    7.10 -    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
    7.11 +   [(@{syntax_const "_alpha"}, K alpha_ast_tr),
    7.12 +    (@{syntax_const "_alpha_ofsort"}, K alpha_ofsort_ast_tr),
    7.13 +    (@{syntax_const "_beta"}, K beta_ast_tr),
    7.14 +    (@{syntax_const "_beta_ofsort"}, K beta_ofsort_ast_tr)]
    7.15    end
    7.16  *}
    7.17  
     8.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Sat May 25 15:44:29 2013 +0200
     8.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sat May 25 18:30:38 2013 +0200
     8.3 @@ -1469,7 +1469,7 @@
     8.4    @{rail "
     8.5    ( @@{command parse_ast_translation} | @@{command parse_translation} |
     8.6      @@{command print_translation} | @@{command typed_print_translation} |
     8.7 -    @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
     8.8 +    @@{command print_ast_translation}) @{syntax text}
     8.9    ;
    8.10    (@@{ML_antiquotation class_syntax} |
    8.11     @@{ML_antiquotation type_syntax} |
    8.12 @@ -1486,31 +1486,31 @@
    8.13  
    8.14    \medskip
    8.15    {\footnotesize
    8.16 -  \begin{tabular}{ll}
    8.17 -  @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
    8.18 -  @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
    8.19 -  @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
    8.20 -  @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\
    8.21 -  @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
    8.22 +  \begin{tabular}{l}
    8.23 +  @{command parse_ast_translation} : \\
    8.24 +  \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
    8.25 +  @{command parse_translation} : \\
    8.26 +  \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
    8.27 +  @{command print_translation} : \\
    8.28 +  \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
    8.29 +  @{command typed_print_translation} : \\
    8.30 +  \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\
    8.31 +  @{command print_ast_translation} : \\
    8.32 +  \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
    8.33    \end{tabular}}
    8.34    \medskip
    8.35  
    8.36    The argument list consists of @{text "(c, tr)"} pairs, where @{text
    8.37    "c"} is the syntax name of the formal entity involved, and @{text
    8.38    "tr"} a function that translates a syntax form @{text "c args"} into
    8.39 -  @{text "tr args"}.  The ML naming convention for parse translations
    8.40 -  is @{text "c_tr"} and for print translations @{text "c_tr'"}.
    8.41 +  @{text "tr ctxt args"} (depending on the context).  The ML naming
    8.42 +  convention for parse translations is @{text "c_tr"} and for print
    8.43 +  translations @{text "c_tr'"}.
    8.44  
    8.45    The @{command_ref print_syntax} command displays the sets of names
    8.46    associated with the translation functions of a theory under @{text
    8.47    "parse_ast_translation"} etc.
    8.48  
    8.49 -  If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is
    8.50 -  given, the corresponding translation functions depend on the current
    8.51 -  theory or proof context as additional argument.  This allows to
    8.52 -  implement advanced syntax mechanisms, as translations functions may
    8.53 -  refer to specific theory declarations or auxiliary proof data.
    8.54 -
    8.55    \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"},
    8.56    @{text "@{const_syntax c}"} inline the authentic syntax name of the
    8.57    given formal entities into the ML source.  This is the
     9.1 --- a/src/FOLP/IFOLP.thy	Sat May 25 15:44:29 2013 +0200
     9.2 +++ b/src/FOLP/IFOLP.thy	Sat May 25 18:30:38 2013 +0200
     9.3 @@ -66,13 +66,13 @@
     9.4  
     9.5  parse_translation {*
     9.6    let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
     9.7 -  in [(@{syntax_const "_Proof"}, proof_tr)] end
     9.8 +  in [(@{syntax_const "_Proof"}, K proof_tr)] end
     9.9  *}
    9.10  
    9.11  (*show_proofs = true displays the proof terms -- they are ENORMOUS*)
    9.12  ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
    9.13  
    9.14 -print_translation (advanced) {*
    9.15 +print_translation {*
    9.16    let
    9.17      fun proof_tr' ctxt [P, p] =
    9.18        if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
    10.1 --- a/src/HOL/Big_Operators.thy	Sat May 25 15:44:29 2013 +0200
    10.2 +++ b/src/HOL/Big_Operators.thy	Sat May 25 18:30:38 2013 +0200
    10.3 @@ -370,7 +370,7 @@
    10.4              Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
    10.5            end
    10.6      | setsum_tr' _ = raise Match;
    10.7 -in [(@{const_syntax setsum}, setsum_tr')] end
    10.8 +in [(@{const_syntax setsum}, K setsum_tr')] end
    10.9  *}
   10.10  
   10.11  text {* TODO These are candidates for generalization *}
    11.1 --- a/src/HOL/Code_Evaluation.thy	Sat May 25 15:44:29 2013 +0200
    11.2 +++ b/src/HOL/Code_Evaluation.thy	Sat May 25 18:30:38 2013 +0200
    11.3 @@ -144,15 +144,15 @@
    11.4  subsubsection {* Obfuscation *}
    11.5  
    11.6  print_translation {*
    11.7 -let
    11.8 -  val term = Const ("<TERM>", dummyT);
    11.9 -  fun tr1' [_, _] = term;
   11.10 -  fun tr2' [] = term;
   11.11 -in
   11.12 -  [(@{const_syntax Const}, tr1'),
   11.13 +  let
   11.14 +    val term = Const ("<TERM>", dummyT);
   11.15 +    fun tr1' _ [_, _] = term;
   11.16 +    fun tr2' _ [] = term;
   11.17 +  in
   11.18 +   [(@{const_syntax Const}, tr1'),
   11.19      (@{const_syntax App}, tr1'),
   11.20      (@{const_syntax dummy_term}, tr2')]
   11.21 -end
   11.22 +  end
   11.23  *}
   11.24  
   11.25  
    12.1 --- a/src/HOL/Groups.thy	Sat May 25 15:44:29 2013 +0200
    12.2 +++ b/src/HOL/Groups.thy	Sat May 25 18:30:38 2013 +0200
    12.3 @@ -121,7 +121,7 @@
    12.4  simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
    12.5  simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
    12.6  
    12.7 -typed_print_translation (advanced) {*
    12.8 +typed_print_translation {*
    12.9    let
   12.10      fun tr' c = (c, fn ctxt => fn T => fn ts =>
   12.11        if not (null ts) orelse T = dummyT orelse
    13.1 --- a/src/HOL/HOL.thy	Sat May 25 15:44:29 2013 +0200
    13.2 +++ b/src/HOL/HOL.thy	Sat May 25 18:30:38 2013 +0200
    13.3 @@ -116,7 +116,7 @@
    13.4  syntax "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    13.5  translations "THE x. P" == "CONST The (%x. P)"
    13.6  print_translation {*
    13.7 -  [(@{const_syntax The}, fn [Abs abs] =>
    13.8 +  [(@{const_syntax The}, fn _ => fn [Abs abs] =>
    13.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
   13.10        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
   13.11  *}  -- {* To avoid eta-contraction of body *}
    14.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat May 25 15:44:29 2013 +0200
    14.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat May 25 18:30:38 2013 +0200
    14.3 @@ -40,7 +40,7 @@
    14.4  *}
    14.5  
    14.6  print_translation {*
    14.7 -  [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
    14.8 +  [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] =>
    14.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
   14.10        in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
   14.11  *}  -- {* To avoid eta-contraction of body *}
   14.12 @@ -61,7 +61,7 @@
   14.13            Ast.fold_ast_p @{syntax_const "_cabs"}
   14.14              (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
   14.15        | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
   14.16 -  in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
   14.17 +  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
   14.18  *}
   14.19  
   14.20  print_ast_translation {*
   14.21 @@ -75,7 +75,7 @@
   14.22        | (xs, body) => Ast.Appl
   14.23            [Ast.Constant @{syntax_const "_Lambda"},
   14.24             Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
   14.25 -  in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
   14.26 +  in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end
   14.27  *}
   14.28  
   14.29  text {* Dummy patterns for continuous abstraction *}
    15.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat May 25 15:44:29 2013 +0200
    15.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat May 25 18:30:38 2013 +0200
    15.3 @@ -131,7 +131,7 @@
    15.4  parse_translation {*
    15.5  (* rewrite (_pat x) => (succeed) *)
    15.6  (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
    15.7 - [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
    15.8 + [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
    15.9    Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
   15.10  *}
   15.11  
   15.12 @@ -164,7 +164,7 @@
   15.13                (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
   15.14            end;
   15.15  
   15.16 -  in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
   15.17 +  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
   15.18  *}
   15.19  
   15.20  translations
    16.1 --- a/src/HOL/Hilbert_Choice.thy	Sat May 25 15:44:29 2013 +0200
    16.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat May 25 18:30:38 2013 +0200
    16.3 @@ -25,7 +25,7 @@
    16.4    "SOME x. P" == "CONST Eps (%x. P)"
    16.5  
    16.6  print_translation {*
    16.7 -  [(@{const_syntax Eps}, fn [Abs abs] =>
    16.8 +  [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
    16.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
   16.10        in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
   16.11  *} -- {* to avoid eta-contraction of body *}
    17.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Sat May 25 15:44:29 2013 +0200
    17.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Sat May 25 18:30:38 2013 +0200
    17.3 @@ -54,8 +54,8 @@
    17.4                   ("{_} // _ // {_}" [0,55,0] 50)
    17.5  
    17.6  ML_file "hoare_syntax.ML"
    17.7 -parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
    17.8 -print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
    17.9 +parse_translation {* [(@{syntax_const "_hoare_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
   17.10 +print_translation {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare"}))] *}
   17.11  
   17.12  
   17.13  lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
    18.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sat May 25 15:44:29 2013 +0200
    18.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sat May 25 18:30:38 2013 +0200
    18.3 @@ -56,9 +56,9 @@
    18.4                   ("{_} // _ // {_}" [0,55,0] 50)
    18.5  
    18.6  ML_file "hoare_syntax.ML"
    18.7 -parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
    18.8 +parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, K Hoare_Syntax.hoare_vars_tr)] *}
    18.9  print_translation
   18.10 -  {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
   18.11 +  {* [(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))] *}
   18.12  
   18.13  
   18.14  (*** The proof rules ***)
    19.1 --- a/src/HOL/Hoare/Separation.thy	Sat May 25 15:44:29 2013 +0200
    19.2 +++ b/src/HOL/Hoare/Separation.thy	Sat May 25 18:30:38 2013 +0200
    19.3 @@ -77,10 +77,10 @@
    19.4  *}
    19.5  
    19.6  parse_translation {*
    19.7 - [(@{syntax_const "_emp"}, emp_tr),
    19.8 -  (@{syntax_const "_singl"}, singl_tr),
    19.9 -  (@{syntax_const "_star"}, star_tr),
   19.10 -  (@{syntax_const "_wand"}, wand_tr)]
   19.11 + [(@{syntax_const "_emp"}, K emp_tr),
   19.12 +  (@{syntax_const "_singl"}, K singl_tr),
   19.13 +  (@{syntax_const "_star"}, K star_tr),
   19.14 +  (@{syntax_const "_wand"}, K wand_tr)]
   19.15  *}
   19.16  
   19.17  text{* Now it looks much better: *}
   19.18 @@ -128,10 +128,10 @@
   19.19  *}
   19.20  
   19.21  print_translation {*
   19.22 - [(@{const_syntax is_empty}, is_empty_tr'),
   19.23 -  (@{const_syntax singl}, singl_tr'),
   19.24 -  (@{const_syntax star}, star_tr'),
   19.25 -  (@{const_syntax wand}, wand_tr')]
   19.26 + [(@{const_syntax is_empty}, K is_empty_tr'),
   19.27 +  (@{const_syntax singl}, K singl_tr'),
   19.28 +  (@{const_syntax star}, K star_tr'),
   19.29 +  (@{const_syntax wand}, K wand_tr')]
   19.30  *}
   19.31  
   19.32  text{* Now the intermediate proof states are also readable: *}
    20.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat May 25 15:44:29 2013 +0200
    20.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Sat May 25 18:30:38 2013 +0200
    20.3 @@ -113,15 +113,15 @@
    20.4  
    20.5      fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
    20.6    in
    20.7 -   [(@{const_syntax Collect}, assert_tr'),
    20.8 -    (@{const_syntax Basic}, assign_tr'),
    20.9 -    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
   20.10 -    (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}),
   20.11 -    (@{const_syntax AnnBasic}, annassign_tr'),
   20.12 -    (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}),
   20.13 -    (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}),
   20.14 -    (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}),
   20.15 -    (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})]
   20.16 +   [(@{const_syntax Collect}, K assert_tr'),
   20.17 +    (@{const_syntax Basic}, K assign_tr'),
   20.18 +    (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
   20.19 +    (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"})),
   20.20 +    (@{const_syntax AnnBasic}, K annassign_tr'),
   20.21 +    (@{const_syntax AnnWhile}, K (annbexp_tr' @{syntax_const "_AnnWhile"})),
   20.22 +    (@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
   20.23 +    (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
   20.24 +    (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
   20.25    end;
   20.26  *}
   20.27  
    21.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Sat May 25 15:44:29 2013 +0200
    21.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Sat May 25 18:30:38 2013 +0200
    21.3 @@ -18,7 +18,7 @@
    21.4    let
    21.5      fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
    21.6        | quote_tr ts = raise TERM ("quote_tr", ts);
    21.7 -  in [(@{syntax_const "_quote"}, quote_tr)] end
    21.8 +  in [(@{syntax_const "_quote"}, K quote_tr)] end
    21.9  *}
   21.10  
   21.11  end
   21.12 \ No newline at end of file
    22.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat May 25 15:44:29 2013 +0200
    22.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat May 25 18:30:38 2013 +0200
    22.3 @@ -72,10 +72,10 @@
    22.4              (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
    22.5        | assign_tr' _ = raise Match;
    22.6    in
    22.7 -   [(@{const_syntax Collect}, assert_tr'),
    22.8 -    (@{const_syntax Basic}, assign_tr'),
    22.9 -    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
   22.10 -    (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
   22.11 +   [(@{const_syntax Collect}, K assert_tr'),
   22.12 +    (@{const_syntax Basic}, K assign_tr'),
   22.13 +    (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
   22.14 +    (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))]
   22.15    end
   22.16  *}
   22.17  
    23.1 --- a/src/HOL/Inductive.thy	Sat May 25 15:44:29 2013 +0200
    23.2 +++ b/src/HOL/Inductive.thy	Sat May 25 18:30:38 2013 +0200
    23.3 @@ -299,14 +299,14 @@
    23.4  syntax (xsymbols)
    23.5    "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    23.6  
    23.7 -parse_translation (advanced) {*
    23.8 -let
    23.9 -  fun fun_tr ctxt [cs] =
   23.10 -    let
   23.11 -      val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
   23.12 -      val ft = Case_Translation.case_tr true ctxt [x, cs];
   23.13 -    in lambda x ft end
   23.14 -in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
   23.15 +parse_translation {*
   23.16 +  let
   23.17 +    fun fun_tr ctxt [cs] =
   23.18 +      let
   23.19 +        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
   23.20 +        val ft = Case_Translation.case_tr true ctxt [x, cs];
   23.21 +      in lambda x ft end
   23.22 +  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
   23.23  *}
   23.24  
   23.25  end
    24.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Sat May 25 15:44:29 2013 +0200
    24.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Sat May 25 18:30:38 2013 +0200
    24.3 @@ -216,7 +216,7 @@
    24.4    let
    24.5      fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
    24.6        | quote_tr ts = raise TERM ("quote_tr", ts);
    24.7 -  in [(@{syntax_const "_quote"}, quote_tr)] end
    24.8 +  in [(@{syntax_const "_quote"}, K quote_tr)] end
    24.9  *}
   24.10  
   24.11  text {* As usual in Isabelle syntax translations, the part for
   24.12 @@ -241,10 +241,10 @@
   24.13              (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   24.14        | assign_tr' _ = raise Match;
   24.15    in
   24.16 -   [(@{const_syntax Collect}, assert_tr'),
   24.17 -    (@{const_syntax Basic}, assign_tr'),
   24.18 -    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
   24.19 -    (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
   24.20 +   [(@{const_syntax Collect}, K assert_tr'),
   24.21 +    (@{const_syntax Basic}, K assign_tr'),
   24.22 +    (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
   24.23 +    (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
   24.24    end
   24.25  *}
   24.26  
    25.1 --- a/src/HOL/Library/Cardinality.thy	Sat May 25 15:44:29 2013 +0200
    25.2 +++ b/src/HOL/Library/Cardinality.thy	Sat May 25 18:30:38 2013 +0200
    25.3 @@ -43,9 +43,9 @@
    25.4  
    25.5  translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    25.6  
    25.7 -typed_print_translation (advanced) {*
    25.8 +print_translation {*
    25.9    let
   25.10 -    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
   25.11 +    fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] =
   25.12        Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
   25.13    in [(@{const_syntax card}, card_univ_tr')] end
   25.14  *}
    26.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat May 25 15:44:29 2013 +0200
    26.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat May 25 18:30:38 2013 +0200
    26.3 @@ -324,7 +324,7 @@
    26.4  code_datatype Num0
    26.5  
    26.6  instantiation num0 :: equal begin
    26.7 -definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool" 
    26.8 +definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
    26.9    where "equal_num0 = op ="
   26.10  instance by intro_classes (simp add: equal_num0_def)
   26.11  end
   26.12 @@ -351,7 +351,7 @@
   26.13  definition "enum_class.enum_ex P = P (1 :: num1)"
   26.14  instance
   26.15    by intro_classes
   26.16 -     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, 
   26.17 +     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
   26.18        (metis (full_types) num1_eq_iff)+)
   26.19  end
   26.20  
   26.21 @@ -477,47 +477,50 @@
   26.22    (type) "0" == (type) "num0"
   26.23  
   26.24  parse_translation {*
   26.25 -let
   26.26 -  fun mk_bintype n =
   26.27 -    let
   26.28 -      fun mk_bit 0 = Syntax.const @{type_syntax bit0}
   26.29 -        | mk_bit 1 = Syntax.const @{type_syntax bit1};
   26.30 -      fun bin_of n =
   26.31 -        if n = 1 then Syntax.const @{type_syntax num1}
   26.32 -        else if n = 0 then Syntax.const @{type_syntax num0}
   26.33 -        else if n = ~1 then raise TERM ("negative type numeral", [])
   26.34 -        else
   26.35 -          let val (q, r) = Integer.div_mod n 2;
   26.36 -          in mk_bit r $ bin_of q end;
   26.37 -    in bin_of n end;
   26.38 +  let
   26.39 +    fun mk_bintype n =
   26.40 +      let
   26.41 +        fun mk_bit 0 = Syntax.const @{type_syntax bit0}
   26.42 +          | mk_bit 1 = Syntax.const @{type_syntax bit1};
   26.43 +        fun bin_of n =
   26.44 +          if n = 1 then Syntax.const @{type_syntax num1}
   26.45 +          else if n = 0 then Syntax.const @{type_syntax num0}
   26.46 +          else if n = ~1 then raise TERM ("negative type numeral", [])
   26.47 +          else
   26.48 +            let val (q, r) = Integer.div_mod n 2;
   26.49 +            in mk_bit r $ bin_of q end;
   26.50 +      in bin_of n end;
   26.51  
   26.52 -  fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
   26.53 -    | numeral_tr ts = raise TERM ("numeral_tr", ts);
   26.54 +    fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
   26.55 +      | numeral_tr ts = raise TERM ("numeral_tr", ts);
   26.56  
   26.57 -in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
   26.58 +  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
   26.59  *}
   26.60  
   26.61  print_translation {*
   26.62 -let
   26.63 -  fun int_of [] = 0
   26.64 -    | int_of (b :: bs) = b + 2 * int_of bs;
   26.65 +  let
   26.66 +    fun int_of [] = 0
   26.67 +      | int_of (b :: bs) = b + 2 * int_of bs;
   26.68  
   26.69 -  fun bin_of (Const (@{type_syntax num0}, _)) = []
   26.70 -    | bin_of (Const (@{type_syntax num1}, _)) = [1]
   26.71 -    | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
   26.72 -    | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
   26.73 -    | bin_of t = raise TERM ("bin_of", [t]);
   26.74 +    fun bin_of (Const (@{type_syntax num0}, _)) = []
   26.75 +      | bin_of (Const (@{type_syntax num1}, _)) = [1]
   26.76 +      | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
   26.77 +      | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
   26.78 +      | bin_of t = raise TERM ("bin_of", [t]);
   26.79  
   26.80 -  fun bit_tr' b [t] =
   26.81 -        let
   26.82 -          val rev_digs = b :: bin_of t handle TERM _ => raise Match
   26.83 -          val i = int_of rev_digs;
   26.84 -          val num = string_of_int (abs i);
   26.85 -        in
   26.86 -          Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   26.87 -        end
   26.88 -    | bit_tr' b _ = raise Match;
   26.89 -in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
   26.90 +    fun bit_tr' b [t] =
   26.91 +          let
   26.92 +            val rev_digs = b :: bin_of t handle TERM _ => raise Match
   26.93 +            val i = int_of rev_digs;
   26.94 +            val num = string_of_int (abs i);
   26.95 +          in
   26.96 +            Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   26.97 +          end
   26.98 +      | bit_tr' b _ = raise Match;
   26.99 +  in
  26.100 +   [(@{type_syntax bit0}, K (bit_tr' 0)),
  26.101 +    (@{type_syntax bit1}, K (bit_tr' 1))]
  26.102 +  end;
  26.103  *}
  26.104  
  26.105  subsection {* Examples *}
    27.1 --- a/src/HOL/Library/Phantom_Type.thy	Sat May 25 15:44:29 2013 +0200
    27.2 +++ b/src/HOL/Library/Phantom_Type.thy	Sat May 25 18:30:38 2013 +0200
    27.3 @@ -27,13 +27,13 @@
    27.4  translations
    27.5    "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
    27.6  
    27.7 -typed_print_translation (advanced) {*
    27.8 -let
    27.9 -  fun phantom_tr' ctxt 
   27.10 -      (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
   27.11 -    Term.list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
   27.12 -  | phantom_tr' _ _ _ = raise Match;
   27.13 -in [(@{const_syntax phantom}, phantom_tr')] end
   27.14 +typed_print_translation {*
   27.15 +  let
   27.16 +    fun phantom_tr' ctxt (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
   27.17 +          list_comb
   27.18 +            (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
   27.19 +      | phantom_tr' _ _ _ = raise Match;
   27.20 +  in [(@{const_syntax phantom}, phantom_tr')] end
   27.21  *}
   27.22  
   27.23  end
    28.1 --- a/src/HOL/List.thy	Sat May 25 15:44:29 2013 +0200
    28.2 +++ b/src/HOL/List.thy	Sat May 25 18:30:38 2013 +0200
    28.3 @@ -386,7 +386,7 @@
    28.4  syntax (HTML output)
    28.5    "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
    28.6  
    28.7 -parse_translation (advanced) {*
    28.8 +parse_translation {*
    28.9    let
   28.10      val NilC = Syntax.const @{const_syntax Nil};
   28.11      val ConsC = Syntax.const @{const_syntax Cons};
    29.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat May 25 15:44:29 2013 +0200
    29.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat May 25 18:30:38 2013 +0200
    29.3 @@ -28,18 +28,19 @@
    29.4  syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
    29.5  
    29.6  parse_translation {*
    29.7 -let
    29.8 -  fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    29.9 -  fun finite_vec_tr [t, u] =
   29.10 -    (case Term_Position.strip_positions u of
   29.11 -      v as Free (x, _) =>
   29.12 -        if Lexicon.is_tid x then
   29.13 -          vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
   29.14 -        else vec t u
   29.15 -    | _ => vec t u)
   29.16 -in
   29.17 -  [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
   29.18 -end
   29.19 +  let
   29.20 +    fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
   29.21 +    fun finite_vec_tr [t, u] =
   29.22 +      (case Term_Position.strip_positions u of
   29.23 +        v as Free (x, _) =>
   29.24 +          if Lexicon.is_tid x then
   29.25 +            vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
   29.26 +              Syntax.const @{class_syntax finite})
   29.27 +          else vec t u
   29.28 +      | _ => vec t u)
   29.29 +  in
   29.30 +    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
   29.31 +  end
   29.32  *}
   29.33  
   29.34  lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    30.1 --- a/src/HOL/Num.thy	Sat May 25 15:44:29 2013 +0200
    30.2 +++ b/src/HOL/Num.thy	Sat May 25 18:30:38 2013 +0200
    30.3 @@ -291,50 +291,54 @@
    30.4    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
    30.5  
    30.6  parse_translation {*
    30.7 -let
    30.8 -  fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
    30.9 -     of (0, 1) => Syntax.const @{const_name One}
   30.10 -      | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
   30.11 -      | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n
   30.12 -    else raise Match;
   30.13 -  val pos = Syntax.const @{const_name numeral}
   30.14 -  val neg = Syntax.const @{const_name neg_numeral}
   30.15 -  val one = Syntax.const @{const_name Groups.one}
   30.16 -  val zero = Syntax.const @{const_name Groups.zero}
   30.17 -  fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   30.18 -        c $ numeral_tr [t] $ u
   30.19 -    | numeral_tr [Const (num, _)] =
   30.20 -        let
   30.21 -          val {value, ...} = Lexicon.read_xnum num;
   30.22 -        in
   30.23 -          if value = 0 then zero else
   30.24 -          if value > 0
   30.25 -          then pos $ num_of_int value
   30.26 -          else neg $ num_of_int (~value)
   30.27 -        end
   30.28 -    | numeral_tr ts = raise TERM ("numeral_tr", ts);
   30.29 -in [("_Numeral", numeral_tr)] end
   30.30 +  let
   30.31 +    fun num_of_int n =
   30.32 +      if n > 0 then
   30.33 +        (case IntInf.quotRem (n, 2) of
   30.34 +          (0, 1) => Syntax.const @{const_name One}
   30.35 +        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
   30.36 +        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
   30.37 +      else raise Match
   30.38 +    val pos = Syntax.const @{const_name numeral}
   30.39 +    val neg = Syntax.const @{const_name neg_numeral}
   30.40 +    val one = Syntax.const @{const_name Groups.one}
   30.41 +    val zero = Syntax.const @{const_name Groups.zero}
   30.42 +    fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   30.43 +          c $ numeral_tr [t] $ u
   30.44 +      | numeral_tr [Const (num, _)] =
   30.45 +          let
   30.46 +            val {value, ...} = Lexicon.read_xnum num;
   30.47 +          in
   30.48 +            if value = 0 then zero else
   30.49 +            if value > 0
   30.50 +            then pos $ num_of_int value
   30.51 +            else neg $ num_of_int (~value)
   30.52 +          end
   30.53 +      | numeral_tr ts = raise TERM ("numeral_tr", ts);
   30.54 +  in [("_Numeral", K numeral_tr)] end
   30.55  *}
   30.56  
   30.57 -typed_print_translation (advanced) {*
   30.58 -let
   30.59 -  fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
   30.60 -    | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
   30.61 -    | dest_num (Const (@{const_syntax One}, _)) = 1;
   30.62 -  fun num_tr' sign ctxt T [n] =
   30.63 -    let
   30.64 -      val k = dest_num n;
   30.65 -      val t' = Syntax.const @{syntax_const "_Numeral"} $
   30.66 -        Syntax.free (sign ^ string_of_int k);
   30.67 -    in
   30.68 -      case T of
   30.69 -        Type (@{type_name fun}, [_, T']) =>
   30.70 -          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
   30.71 -          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
   30.72 -      | T' => if T' = dummyT then t' else raise Match
   30.73 -    end;
   30.74 -in [(@{const_syntax numeral}, num_tr' ""),
   30.75 -    (@{const_syntax neg_numeral}, num_tr' "-")] end
   30.76 +typed_print_translation {*
   30.77 +  let
   30.78 +    fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
   30.79 +      | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
   30.80 +      | dest_num (Const (@{const_syntax One}, _)) = 1;
   30.81 +    fun num_tr' sign ctxt T [n] =
   30.82 +      let
   30.83 +        val k = dest_num n;
   30.84 +        val t' = Syntax.const @{syntax_const "_Numeral"} $
   30.85 +          Syntax.free (sign ^ string_of_int k);
   30.86 +      in
   30.87 +        (case T of
   30.88 +          Type (@{type_name fun}, [_, T']) =>
   30.89 +            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
   30.90 +            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
   30.91 +        | T' => if T' = dummyT then t' else raise Match)
   30.92 +      end;
   30.93 +  in
   30.94 +   [(@{const_syntax numeral}, num_tr' ""),
   30.95 +    (@{const_syntax neg_numeral}, num_tr' "-")]
   30.96 +  end
   30.97  *}
   30.98  
   30.99  ML_file "Tools/numeral.ML"
    31.1 --- a/src/HOL/Orderings.thy	Sat May 25 15:44:29 2013 +0200
    31.2 +++ b/src/HOL/Orderings.thy	Sat May 25 18:30:38 2013 +0200
    31.3 @@ -727,8 +727,8 @@
    31.4    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
    31.5    fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
    31.6  
    31.7 -  fun tr' q = (q,
    31.8 -    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
    31.9 +  fun tr' q = (q, fn _ =>
   31.10 +    (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
   31.11          Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
   31.12          (case AList.lookup (op =) trans (q, c, d) of
   31.13            NONE => raise Match
   31.14 @@ -736,7 +736,7 @@
   31.15              if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
   31.16              else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
   31.17              else raise Match)
   31.18 -     | _ => raise Match);
   31.19 +      | _ => raise Match));
   31.20  in [tr' All_binder, tr' Ex_binder] end
   31.21  *}
   31.22  
    32.1 --- a/src/HOL/Product_Type.thy	Sat May 25 15:44:29 2013 +0200
    32.2 +++ b/src/HOL/Product_Type.thy	Sat May 25 18:30:38 2013 +0200
    32.3 @@ -196,71 +196,71 @@
    32.4  (*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
    32.5    works best with enclosing "let", if "let" does not avoid eta-contraction*)
    32.6  print_translation {*
    32.7 -let
    32.8 -  fun split_tr' [Abs (x, T, t as (Abs abs))] =
    32.9 -        (* split (%x y. t) => %(x,y) t *)
   32.10 -        let
   32.11 -          val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
   32.12 -          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   32.13 -        in
   32.14 -          Syntax.const @{syntax_const "_abs"} $
   32.15 -            (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   32.16 -        end
   32.17 -    | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
   32.18 -        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   32.19 -        let
   32.20 -          val Const (@{syntax_const "_abs"}, _) $
   32.21 -            (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
   32.22 -          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   32.23 -        in
   32.24 -          Syntax.const @{syntax_const "_abs"} $
   32.25 -            (Syntax.const @{syntax_const "_pattern"} $ x' $
   32.26 -              (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
   32.27 -        end
   32.28 -    | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
   32.29 -        (* split (split (%x y z. t)) => %((x, y), z). t *)
   32.30 -        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   32.31 -    | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   32.32 -        (* split (%pttrn z. t) => %(pttrn,z). t *)
   32.33 -        let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
   32.34 -          Syntax.const @{syntax_const "_abs"} $
   32.35 -            (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   32.36 -        end
   32.37 -    | split_tr' _ = raise Match;
   32.38 -in [(@{const_syntax prod_case}, split_tr')] end
   32.39 +  let
   32.40 +    fun split_tr' [Abs (x, T, t as (Abs abs))] =
   32.41 +          (* split (%x y. t) => %(x,y) t *)
   32.42 +          let
   32.43 +            val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
   32.44 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   32.45 +          in
   32.46 +            Syntax.const @{syntax_const "_abs"} $
   32.47 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   32.48 +          end
   32.49 +      | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
   32.50 +          (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   32.51 +          let
   32.52 +            val Const (@{syntax_const "_abs"}, _) $
   32.53 +              (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
   32.54 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   32.55 +          in
   32.56 +            Syntax.const @{syntax_const "_abs"} $
   32.57 +              (Syntax.const @{syntax_const "_pattern"} $ x' $
   32.58 +                (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
   32.59 +          end
   32.60 +      | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
   32.61 +          (* split (split (%x y z. t)) => %((x, y), z). t *)
   32.62 +          split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   32.63 +      | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   32.64 +          (* split (%pttrn z. t) => %(pttrn,z). t *)
   32.65 +          let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
   32.66 +            Syntax.const @{syntax_const "_abs"} $
   32.67 +              (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   32.68 +          end
   32.69 +      | split_tr' _ = raise Match;
   32.70 +  in [(@{const_syntax prod_case}, K split_tr')] end
   32.71  *}
   32.72  
   32.73  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   32.74  typed_print_translation {*
   32.75 -let
   32.76 -  fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
   32.77 -    | split_guess_names_tr' T [Abs (x, xT, t)] =
   32.78 -        (case (head_of t) of
   32.79 -          Const (@{const_syntax prod_case}, _) => raise Match
   32.80 -        | _ =>
   32.81 -          let 
   32.82 -            val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   32.83 -            val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
   32.84 -            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
   32.85 -          in
   32.86 -            Syntax.const @{syntax_const "_abs"} $
   32.87 -              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   32.88 -          end)
   32.89 -    | split_guess_names_tr' T [t] =
   32.90 -        (case head_of t of
   32.91 -          Const (@{const_syntax prod_case}, _) => raise Match
   32.92 -        | _ =>
   32.93 -          let
   32.94 -            val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   32.95 -            val (y, t') =
   32.96 -              Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
   32.97 -            val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
   32.98 -          in
   32.99 -            Syntax.const @{syntax_const "_abs"} $
  32.100 -              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
  32.101 -          end)
  32.102 -    | split_guess_names_tr' _ _ = raise Match;
  32.103 -in [(@{const_syntax prod_case}, split_guess_names_tr')] end
  32.104 +  let
  32.105 +    fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
  32.106 +      | split_guess_names_tr' T [Abs (x, xT, t)] =
  32.107 +          (case (head_of t) of
  32.108 +            Const (@{const_syntax prod_case}, _) => raise Match
  32.109 +          | _ =>
  32.110 +            let 
  32.111 +              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
  32.112 +              val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
  32.113 +              val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
  32.114 +            in
  32.115 +              Syntax.const @{syntax_const "_abs"} $
  32.116 +                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
  32.117 +            end)
  32.118 +      | split_guess_names_tr' T [t] =
  32.119 +          (case head_of t of
  32.120 +            Const (@{const_syntax prod_case}, _) => raise Match
  32.121 +          | _ =>
  32.122 +            let
  32.123 +              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
  32.124 +              val (y, t') =
  32.125 +                Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
  32.126 +              val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
  32.127 +            in
  32.128 +              Syntax.const @{syntax_const "_abs"} $
  32.129 +                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
  32.130 +            end)
  32.131 +      | split_guess_names_tr' _ _ = raise Match;
  32.132 +  in [(@{const_syntax prod_case}, K split_guess_names_tr')] end
  32.133  *}
  32.134  
  32.135  (* Force eta-contraction for terms of the form "Q A (%p. prod_case P p)"
  32.136 @@ -270,19 +270,20 @@
  32.137     Otherwise prevent eta-contraction.
  32.138  *)
  32.139  print_translation {*
  32.140 -let
  32.141 -  fun contract Q f ts =
  32.142 -    case ts of
  32.143 -      [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
  32.144 -      => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
  32.145 -    | _ => f ts;
  32.146 -  fun contract2 (Q,f) = (Q, contract Q f);
  32.147 -  val pairs =
  32.148 +  let
  32.149 +    fun contract Q tr ctxt ts =
  32.150 +      (case ts of
  32.151 +        [A, Abs (_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] =>
  32.152 +          if Term.is_dependent t then tr ctxt ts
  32.153 +          else Syntax.const Q $ A $ s
  32.154 +      | _ => tr ctxt ts);
  32.155 +  in
  32.156      [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
  32.157       Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
  32.158       Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
  32.159       Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
  32.160 -in map contract2 pairs end
  32.161 +    |> map (fn (Q, tr) => (Q, contract Q tr))
  32.162 +  end
  32.163  *}
  32.164  
  32.165  subsubsection {* Code generator setup *}
    33.1 --- a/src/HOL/Rat.thy	Sat May 25 15:44:29 2013 +0200
    33.2 +++ b/src/HOL/Rat.thy	Sat May 25 18:30:38 2013 +0200
    33.3 @@ -341,7 +341,7 @@
    33.4  proof -
    33.5    have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
    33.6      by (rule sym) (auto intro: normalize_eq)
    33.7 -  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
    33.8 +  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
    33.9      by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   33.10    moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
   33.11      by (rule normalize_coprime) simp
   33.12 @@ -1106,16 +1106,42 @@
   33.13    ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
   33.14    uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
   33.15  
   33.16 -subsection{* Float syntax *}
   33.17 +
   33.18 +subsection {* Float syntax *}
   33.19  
   33.20  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
   33.21  
   33.22 -ML_file "Tools/float_syntax.ML"
   33.23 -setup Float_Syntax.setup
   33.24 +parse_translation {*
   33.25 +  let
   33.26 +    fun mk_number i =
   33.27 +      let
   33.28 +        fun mk 1 = Syntax.const @{const_syntax Num.One}
   33.29 +          | mk i =
   33.30 +              let val (q, r) = Integer.div_mod i 2
   33.31 +              in HOLogic.mk_bit r $ (mk q) end;
   33.32 +      in
   33.33 +        if i = 0 then Syntax.const @{const_syntax Groups.zero}
   33.34 +        else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
   33.35 +        else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
   33.36 +      end;
   33.37 +
   33.38 +    fun mk_frac str =
   33.39 +      let
   33.40 +        val {mant = i, exp = n} = Lexicon.read_float str;
   33.41 +        val exp = Syntax.const @{const_syntax Power.power};
   33.42 +        val ten = mk_number 10;
   33.43 +        val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
   33.44 +      in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
   33.45 +
   33.46 +    fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
   33.47 +      | float_tr [t as Const (str, _)] = mk_frac str
   33.48 +      | float_tr ts = raise TERM ("float_tr", ts);
   33.49 +  in [(@{syntax_const "_Float"}, K float_tr)] end
   33.50 +*}
   33.51  
   33.52  text{* Test: *}
   33.53  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
   33.54 -by simp
   33.55 +  by simp
   33.56  
   33.57  
   33.58  hide_const (open) normalize positive
    34.1 --- a/src/HOL/Set.thy	Sat May 25 15:44:29 2013 +0200
    34.2 +++ b/src/HOL/Set.thy	Sat May 25 18:30:38 2013 +0200
    34.3 @@ -256,35 +256,36 @@
    34.4   "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
    34.5  
    34.6  print_translation {*
    34.7 -let
    34.8 -  val All_binder = Mixfix.binder_name @{const_syntax All};
    34.9 -  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
   34.10 -  val impl = @{const_syntax HOL.implies};
   34.11 -  val conj = @{const_syntax HOL.conj};
   34.12 -  val sbset = @{const_syntax subset};
   34.13 -  val sbset_eq = @{const_syntax subset_eq};
   34.14 -
   34.15 -  val trans =
   34.16 -   [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
   34.17 -    ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
   34.18 -    ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
   34.19 -    ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
   34.20 -
   34.21 -  fun mk v (v', T) c n P =
   34.22 -    if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
   34.23 -    then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P else raise Match;
   34.24 -
   34.25 -  fun tr' q = (q,
   34.26 -        fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
   34.27 -            Const (c, _) $
   34.28 -              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
   34.29 -            (case AList.lookup (op =) trans (q, c, d) of
   34.30 -              NONE => raise Match
   34.31 -            | SOME l => mk v (v', T) l n P)
   34.32 -         | _ => raise Match);
   34.33 -in
   34.34 -  [tr' All_binder, tr' Ex_binder]
   34.35 -end
   34.36 +  let
   34.37 +    val All_binder = Mixfix.binder_name @{const_syntax All};
   34.38 +    val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
   34.39 +    val impl = @{const_syntax HOL.implies};
   34.40 +    val conj = @{const_syntax HOL.conj};
   34.41 +    val sbset = @{const_syntax subset};
   34.42 +    val sbset_eq = @{const_syntax subset_eq};
   34.43 +
   34.44 +    val trans =
   34.45 +     [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
   34.46 +      ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
   34.47 +      ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
   34.48 +      ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
   34.49 +
   34.50 +    fun mk v (v', T) c n P =
   34.51 +      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
   34.52 +      then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
   34.53 +      else raise Match;
   34.54 +
   34.55 +    fun tr' q = (q, fn _ =>
   34.56 +      (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
   34.57 +          Const (c, _) $
   34.58 +            (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
   34.59 +          (case AList.lookup (op =) trans (q, c, d) of
   34.60 +            NONE => raise Match
   34.61 +          | SOME l => mk v (v', T) l n P)
   34.62 +        | _ => raise Match));
   34.63 +  in
   34.64 +    [tr' All_binder, tr' Ex_binder]
   34.65 +  end
   34.66  *}
   34.67  
   34.68  
   34.69 @@ -304,11 +305,11 @@
   34.70      fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
   34.71        | nvars _ = 1;
   34.72  
   34.73 -    fun setcompr_tr [e, idts, b] =
   34.74 +    fun setcompr_tr ctxt [e, idts, b] =
   34.75        let
   34.76          val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
   34.77          val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
   34.78 -        val exP = ex_tr [idts, P];
   34.79 +        val exP = ex_tr ctxt [idts, P];
   34.80        in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
   34.81  
   34.82    in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
   34.83 @@ -323,7 +324,7 @@
   34.84  let
   34.85    val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
   34.86  
   34.87 -  fun setcompr_tr' [Abs (abs as (_, _, P))] =
   34.88 +  fun setcompr_tr' ctxt [Abs (abs as (_, _, P))] =
   34.89      let
   34.90        fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
   34.91          | check (Const (@{const_syntax HOL.conj}, _) $
   34.92 @@ -333,7 +334,7 @@
   34.93          | check _ = false;
   34.94  
   34.95          fun tr' (_ $ abs) =
   34.96 -          let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
   34.97 +          let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' ctxt [abs]
   34.98            in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
   34.99      in
  34.100        if check (P, 0) then tr' P
  34.101 @@ -1004,7 +1005,7 @@
  34.102  lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
  34.103    by (unfold less_le) blast
  34.104  
  34.105 -lemma psubsetE [elim!,no_atp]: 
  34.106 +lemma psubsetE [elim!,no_atp]:
  34.107      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
  34.108    by (unfold less_le) blast
  34.109  
  34.110 @@ -1758,10 +1759,10 @@
  34.111  lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
  34.112    by auto
  34.113  
  34.114 -lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) = 
  34.115 +lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) =
  34.116     (if c \<in> A then (if d \<in> A then UNIV else B)
  34.117 -    else if d \<in> A then -B else {})"  
  34.118 -  by (auto simp add: vimage_def) 
  34.119 +    else if d \<in> A then -B else {})"
  34.120 +  by (auto simp add: vimage_def)
  34.121  
  34.122  lemma vimage_inter_cong:
  34.123    "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
    35.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Sat May 25 15:44:29 2013 +0200
    35.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Sat May 25 18:30:38 2013 +0200
    35.3 @@ -21,14 +21,14 @@
    35.4    "s<x:=y>" == "_statespace_update s x y"
    35.5  
    35.6  
    35.7 -parse_translation (advanced)
    35.8 +parse_translation
    35.9  {*
   35.10   [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
   35.11    (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
   35.12  *}
   35.13  
   35.14  
   35.15 -print_translation (advanced)
   35.16 +print_translation
   35.17  {*
   35.18   [(@{const_syntax lookup}, StateSpace.lookup_tr'),
   35.19    (@{const_syntax update}, StateSpace.update_tr')]
    36.1 --- a/src/HOL/Tools/case_translation.ML	Sat May 25 15:44:29 2013 +0200
    36.2 +++ b/src/HOL/Tools/case_translation.ML	Sat May 25 18:30:38 2013 +0200
    36.3 @@ -148,10 +148,7 @@
    36.4        end
    36.5    | case_tr _ _ _ = case_error "case_tr";
    36.6  
    36.7 -val trfun_setup =
    36.8 -  Sign.add_advanced_trfuns ([],
    36.9 -    [(@{syntax_const "_case_syntax"}, case_tr true)],
   36.10 -    [], []);
   36.11 +val trfun_setup = Sign.parse_translation [(@{syntax_const "_case_syntax"}, case_tr true)];
   36.12  
   36.13  
   36.14  (* print translation *)
   36.15 @@ -176,8 +173,7 @@
   36.16              (mk_clauses t), ts)
   36.17        end;
   36.18  
   36.19 -val trfun_setup' = Sign.add_trfuns
   36.20 -  ([], [], [(@{const_syntax "case_guard"}, case_tr')], []);
   36.21 +val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
   36.22  
   36.23  
   36.24  (* declarations *)
    37.1 --- a/src/HOL/Tools/float_syntax.ML	Sat May 25 15:44:29 2013 +0200
    37.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.3 @@ -1,53 +0,0 @@
    37.4 -(*  Title:      HOL/Tools/float_syntax.ML
    37.5 -    Author:     Tobias Nipkow, TU Muenchen
    37.6 -
    37.7 -Concrete syntax for floats.
    37.8 -*)
    37.9 -
   37.10 -signature FLOAT_SYNTAX =
   37.11 -sig
   37.12 -  val setup: theory -> theory
   37.13 -end;
   37.14 -
   37.15 -structure Float_Syntax: FLOAT_SYNTAX =
   37.16 -struct
   37.17 -
   37.18 -(* parse translation *)
   37.19 -
   37.20 -local
   37.21 -
   37.22 -fun mk_number i =
   37.23 -  let
   37.24 -    fun mk 1 = Syntax.const @{const_syntax Num.One}
   37.25 -      | mk i =
   37.26 -          let val (q, r) = Integer.div_mod i 2
   37.27 -          in HOLogic.mk_bit r $ (mk q) end;
   37.28 -  in
   37.29 -    if i = 0 then Syntax.const @{const_syntax Groups.zero}
   37.30 -    else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
   37.31 -    else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
   37.32 -  end;
   37.33 -
   37.34 -fun mk_frac str =
   37.35 -  let
   37.36 -    val {mant = i, exp = n} = Lexicon.read_float str;
   37.37 -    val exp = Syntax.const @{const_syntax Power.power};
   37.38 -    val ten = mk_number 10;
   37.39 -    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
   37.40 -  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
   37.41 -
   37.42 -in
   37.43 -
   37.44 -fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
   37.45 -  | float_tr [t as Const (str, _)] = mk_frac str
   37.46 -  | float_tr ts = raise TERM ("float_tr", ts);
   37.47 -
   37.48 -end;
   37.49 -
   37.50 -
   37.51 -(* theory setup *)
   37.52 -
   37.53 -val setup =
   37.54 -  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
   37.55 -
   37.56 -end;
    38.1 --- a/src/HOL/Tools/record.ML	Sat May 25 15:44:29 2013 +0200
    38.2 +++ b/src/HOL/Tools/record.ML	Sat May 25 18:30:38 2013 +0200
    38.3 @@ -735,10 +735,8 @@
    38.4  in
    38.5  
    38.6  val parse_translation =
    38.7 - [(@{syntax_const "_record_update"}, record_update_tr)];
    38.8 -
    38.9 -val advanced_parse_translation =
   38.10 - [(@{syntax_const "_record"}, record_tr),
   38.11 + [(@{syntax_const "_record_update"}, K record_update_tr),
   38.12 +  (@{syntax_const "_record"}, record_tr),
   38.13    (@{syntax_const "_record_scheme"}, record_scheme_tr),
   38.14    (@{syntax_const "_record_type"}, record_type_tr),
   38.15    (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
   38.16 @@ -1896,7 +1894,7 @@
   38.17          val trnames = if parent_len > 0 then [extension_name] else [];
   38.18        in map record_ext_type_tr' trnames end;
   38.19  
   38.20 -    val advanced_print_translation =
   38.21 +    val print_translation =
   38.22        map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
   38.23        record_ext_type_tr's @ record_ext_type_abbr_tr's;
   38.24  
   38.25 @@ -1995,7 +1993,7 @@
   38.26        timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
   38.27          (fn () =>
   38.28            ext_thy
   38.29 -          |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
   38.30 +          |> Sign.print_translation print_translation
   38.31            |> Sign.restore_naming thy
   38.32            |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
   38.33            |> Typedecl.abbrev_global
   38.34 @@ -2316,8 +2314,7 @@
   38.35  (* setup theory *)
   38.36  
   38.37  val setup =
   38.38 -  Sign.add_trfuns ([], parse_translation, [], []) #>
   38.39 -  Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
   38.40 +  Sign.parse_translation parse_translation #>
   38.41    map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
   38.42  
   38.43  
    39.1 --- a/src/HOL/Tools/string_syntax.ML	Sat May 25 15:44:29 2013 +0200
    39.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat May 25 18:30:38 2013 +0200
    39.3 @@ -87,8 +87,11 @@
    39.4  (* theory setup *)
    39.5  
    39.6  val setup =
    39.7 -  Sign.add_trfuns
    39.8 -   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
    39.9 -    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
   39.10 +  Sign.parse_ast_translation
   39.11 +   [(@{syntax_const "_Char"}, K char_ast_tr),
   39.12 +    (@{syntax_const "_String"}, K string_ast_tr)] #>
   39.13 +  Sign.print_ast_translation
   39.14 +   [(@{const_syntax Char}, K char_ast_tr'),
   39.15 +    (@{syntax_const "_list"}, K list_ast_tr')];
   39.16  
   39.17  end;
    40.1 --- a/src/HOL/Typerep.thy	Sat May 25 15:44:29 2013 +0200
    40.2 +++ b/src/HOL/Typerep.thy	Sat May 25 18:30:38 2013 +0200
    40.3 @@ -21,24 +21,24 @@
    40.4    "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
    40.5  
    40.6  parse_translation {*
    40.7 -let
    40.8 -  fun typerep_tr (*"_TYPEREP"*) [ty] =
    40.9 -        Syntax.const @{const_syntax typerep} $
   40.10 -          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
   40.11 -            (Syntax.const @{type_syntax itself} $ ty))
   40.12 -    | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
   40.13 -in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
   40.14 +  let
   40.15 +    fun typerep_tr (*"_TYPEREP"*) [ty] =
   40.16 +          Syntax.const @{const_syntax typerep} $
   40.17 +            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
   40.18 +              (Syntax.const @{type_syntax itself} $ ty))
   40.19 +      | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
   40.20 +  in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
   40.21  *}
   40.22  
   40.23 -typed_print_translation (advanced) {*
   40.24 -let
   40.25 -  fun typerep_tr' ctxt (*"typerep"*)
   40.26 -          (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
   40.27 -          (Const (@{const_syntax TYPE}, _) :: ts) =
   40.28 -        Term.list_comb
   40.29 -          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
   40.30 -    | typerep_tr' _ T ts = raise Match;
   40.31 -in [(@{const_syntax typerep}, typerep_tr')] end
   40.32 +typed_print_translation {*
   40.33 +  let
   40.34 +    fun typerep_tr' ctxt (*"typerep"*)
   40.35 +            (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
   40.36 +            (Const (@{const_syntax TYPE}, _) :: ts) =
   40.37 +          Term.list_comb
   40.38 +            (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
   40.39 +      | typerep_tr' _ T ts = raise Match;
   40.40 +  in [(@{const_syntax typerep}, typerep_tr')] end
   40.41  *}
   40.42  
   40.43  setup {*
    41.1 --- a/src/HOL/ex/Binary.thy	Sat May 25 15:44:29 2013 +0200
    41.2 +++ b/src/HOL/ex/Binary.thy	Sat May 25 18:30:38 2013 +0200
    41.3 @@ -85,7 +85,7 @@
    41.4    shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
    41.5      and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
    41.6    by simp_all
    41.7 -  
    41.8 +
    41.9  lemma binary_less:
   41.10    fixes n :: nat
   41.11    shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
   41.12 @@ -191,19 +191,19 @@
   41.13    "_Binary" :: "num_const \<Rightarrow> 'a"    ("$_")
   41.14  
   41.15  parse_translation {*
   41.16 -let
   41.17 -  val syntax_consts =
   41.18 -    map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
   41.19 +  let
   41.20 +    val syntax_consts =
   41.21 +      map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
   41.22  
   41.23 -  fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
   41.24 -    | binary_tr [Const (num, _)] =
   41.25 -        let
   41.26 -          val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
   41.27 -          val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   41.28 -        in syntax_consts (mk_binary n) end
   41.29 -    | binary_tr ts = raise TERM ("binary_tr", ts);
   41.30 +    fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
   41.31 +      | binary_tr [Const (num, _)] =
   41.32 +          let
   41.33 +            val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
   41.34 +            val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   41.35 +          in syntax_consts (mk_binary n) end
   41.36 +      | binary_tr ts = raise TERM ("binary_tr", ts);
   41.37  
   41.38 -in [(@{syntax_const "_Binary"}, binary_tr)] end
   41.39 +  in [(@{syntax_const "_Binary"}, K binary_tr)] end
   41.40  *}
   41.41  
   41.42  
    42.1 --- a/src/HOL/ex/Multiquote.thy	Sat May 25 15:44:29 2013 +0200
    42.2 +++ b/src/HOL/ex/Multiquote.thy	Sat May 25 18:30:38 2013 +0200
    42.3 @@ -32,7 +32,7 @@
    42.4  
    42.5      fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    42.6        | quote_tr ts = raise TERM ("quote_tr", ts);
    42.7 -  in [(@{syntax_const "_quote"}, quote_tr)] end
    42.8 +  in [(@{syntax_const "_quote"}, K quote_tr)] end
    42.9  *}
   42.10  
   42.11  text {* basic examples *}
    43.1 --- a/src/HOL/ex/Numeral_Representation.thy	Sat May 25 15:44:29 2013 +0200
    43.2 +++ b/src/HOL/ex/Numeral_Representation.thy	Sat May 25 18:30:38 2013 +0200
    43.3 @@ -277,42 +277,42 @@
    43.4    "_Numerals" :: "xnum_token \<Rightarrow> 'a"    ("_")
    43.5  
    43.6  parse_translation {*
    43.7 -let
    43.8 -  fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
    43.9 -     of (0, 1) => Const (@{const_name One}, dummyT)
   43.10 -      | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
   43.11 -      | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
   43.12 -    else raise Match;
   43.13 -  fun numeral_tr [Free (num, _)] =
   43.14 -        let
   43.15 -          val {leading_zeros, value, ...} = Lexicon.read_xnum num;
   43.16 -          val _ = leading_zeros = 0 andalso value > 0
   43.17 -            orelse error ("Bad numeral: " ^ num);
   43.18 -        in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
   43.19 -    | numeral_tr ts = raise TERM ("numeral_tr", ts);
   43.20 -in [(@{syntax_const "_Numerals"}, numeral_tr)] end
   43.21 +  let
   43.22 +    fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
   43.23 +       of (0, 1) => Const (@{const_name One}, dummyT)
   43.24 +        | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
   43.25 +        | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
   43.26 +      else raise Match;
   43.27 +    fun numeral_tr [Free (num, _)] =
   43.28 +          let
   43.29 +            val {leading_zeros, value, ...} = Lexicon.read_xnum num;
   43.30 +            val _ = leading_zeros = 0 andalso value > 0
   43.31 +              orelse error ("Bad numeral: " ^ num);
   43.32 +          in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
   43.33 +      | numeral_tr ts = raise TERM ("numeral_tr", ts);
   43.34 +  in [(@{syntax_const "_Numerals"}, K numeral_tr)] end
   43.35  *}
   43.36  
   43.37 -typed_print_translation (advanced) {*
   43.38 -let
   43.39 -  fun dig b n = b + 2 * n; 
   43.40 -  fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
   43.41 -        dig 0 (int_of_num' n)
   43.42 -    | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
   43.43 -        dig 1 (int_of_num' n)
   43.44 -    | int_of_num' (Const (@{const_syntax One}, _)) = 1;
   43.45 -  fun num_tr' ctxt T [n] =
   43.46 -    let
   43.47 -      val k = int_of_num' n;
   43.48 -      val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
   43.49 -    in
   43.50 -      case T of
   43.51 -        Type (@{type_name fun}, [_, T']) =>
   43.52 -          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
   43.53 -          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
   43.54 -      | T' => if T' = dummyT then t' else raise Match
   43.55 -    end;
   43.56 -in [(@{const_syntax of_num}, num_tr')] end
   43.57 +typed_print_translation {*
   43.58 +  let
   43.59 +    fun dig b n = b + 2 * n; 
   43.60 +    fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
   43.61 +          dig 0 (int_of_num' n)
   43.62 +      | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
   43.63 +          dig 1 (int_of_num' n)
   43.64 +      | int_of_num' (Const (@{const_syntax One}, _)) = 1;
   43.65 +    fun num_tr' ctxt T [n] =
   43.66 +      let
   43.67 +        val k = int_of_num' n;
   43.68 +        val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
   43.69 +      in
   43.70 +        case T of
   43.71 +          Type (@{type_name fun}, [_, T']) =>
   43.72 +            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
   43.73 +            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
   43.74 +        | T' => if T' = dummyT then t' else raise Match
   43.75 +      end;
   43.76 +  in [(@{const_syntax of_num}, num_tr')] end
   43.77  *}
   43.78  
   43.79  
    44.1 --- a/src/Pure/Isar/expression.ML	Sat May 25 15:44:29 2013 +0200
    44.2 +++ b/src/Pure/Isar/expression.ML	Sat May 25 18:30:38 2013 +0200
    44.3 @@ -622,7 +622,7 @@
    44.4  fun aprop_tr' n c =
    44.5    let
    44.6      val c' = Lexicon.mark_const c;
    44.7 -    fun tr' T args =
    44.8 +    fun tr' (_: Proof.context) T args =
    44.9        if T <> dummyT andalso length args = n
   44.10        then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
   44.11        else raise Match;
   44.12 @@ -656,7 +656,7 @@
   44.13  
   44.14      val ([pred_def], defs_thy) =
   44.15        thy
   44.16 -      |> bodyT = propT ? Sign.add_trfunsT [aprop_tr' (length args) name]
   44.17 +      |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
   44.18        |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
   44.19        |> Global_Theory.add_defs false
   44.20          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
    45.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat May 25 15:44:29 2013 +0200
    45.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat May 25 18:30:38 2013 +0200
    45.3 @@ -8,11 +8,11 @@
    45.4  sig
    45.5    val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
    45.6    val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
    45.7 -  val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    45.8 -  val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    45.9 -  val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   45.10 -  val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   45.11 -  val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   45.12 +  val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
   45.13 +  val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
   45.14 +  val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
   45.15 +  val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
   45.16 +  val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
   45.17    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   45.18    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   45.19    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   45.20 @@ -85,57 +85,41 @@
   45.21  
   45.22  (* translation functions *)
   45.23  
   45.24 -local
   45.25 -
   45.26 -fun advancedT false = ""
   45.27 -  | advancedT true = "Proof.context -> ";
   45.28 -
   45.29 -fun advancedN false = ""
   45.30 -  | advancedN true = "advanced_";
   45.31 -
   45.32 -in
   45.33 -
   45.34 -fun parse_ast_translation (a, (txt, pos)) =
   45.35 +fun parse_ast_translation (txt, pos) =
   45.36    ML_Lex.read pos txt
   45.37    |> ML_Context.expression pos
   45.38 -    ("val parse_ast_translation: (string * (" ^ advancedT a ^
   45.39 -      "Ast.ast list -> Ast.ast)) list")
   45.40 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   45.41 +    "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   45.42 +    "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
   45.43    |> Context.theory_map;
   45.44  
   45.45 -fun parse_translation (a, (txt, pos)) =
   45.46 +fun parse_translation (txt, pos) =
   45.47 +  ML_Lex.read pos txt
   45.48 +  |> ML_Context.expression pos
   45.49 +    "val parse_translation: (string * (Proof.context -> term list -> term)) list"
   45.50 +    "Context.map_theory (Sign.parse_translation parse_translation)"
   45.51 +  |> Context.theory_map;
   45.52 +
   45.53 +fun print_translation (txt, pos) =
   45.54    ML_Lex.read pos txt
   45.55    |> ML_Context.expression pos
   45.56 -    ("val parse_translation: (string * (" ^ advancedT a ^
   45.57 -      "term list -> term)) list")
   45.58 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
   45.59 -  |> Context.theory_map;
   45.60 -
   45.61 -fun print_translation (a, (txt, pos)) =
   45.62 -  ML_Lex.read pos txt
   45.63 -  |> ML_Context.expression pos
   45.64 -    ("val print_translation: (string * (" ^ advancedT a ^
   45.65 -      "term list -> term)) list")
   45.66 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
   45.67 +    "val print_translation: (string * (Proof.context -> term list -> term)) list"
   45.68 +    "Context.map_theory (Sign.print_translation print_translation)"
   45.69    |> Context.theory_map;
   45.70  
   45.71 -fun print_ast_translation (a, (txt, pos)) =
   45.72 +fun typed_print_translation (txt, pos) =
   45.73    ML_Lex.read pos txt
   45.74    |> ML_Context.expression pos
   45.75 -    ("val print_ast_translation: (string * (" ^ advancedT a ^
   45.76 -      "Ast.ast list -> Ast.ast)) list")
   45.77 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   45.78 +    "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
   45.79 +    "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   45.80    |> Context.theory_map;
   45.81  
   45.82 -fun typed_print_translation (a, (txt, pos)) =
   45.83 +fun print_ast_translation (txt, pos) =
   45.84    ML_Lex.read pos txt
   45.85    |> ML_Context.expression pos
   45.86 -    ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
   45.87 -    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   45.88 +    "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   45.89 +    "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   45.90    |> Context.theory_map;
   45.91  
   45.92 -end;
   45.93 -
   45.94  
   45.95  (* translation rules *)
   45.96  
    46.1 --- a/src/Pure/Isar/isar_syn.ML	Sat May 25 15:44:29 2013 +0200
    46.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat May 25 18:30:38 2013 +0200
    46.3 @@ -323,32 +323,30 @@
    46.4  
    46.5  (* translation functions *)
    46.6  
    46.7 -val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
    46.8 -
    46.9  val _ =
   46.10    Outer_Syntax.command @{command_spec "parse_ast_translation"}
   46.11      "install parse ast translation functions"
   46.12 -    (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
   46.13 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
   46.14  
   46.15  val _ =
   46.16    Outer_Syntax.command @{command_spec "parse_translation"}
   46.17      "install parse translation functions"
   46.18 -    (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
   46.19 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
   46.20  
   46.21  val _ =
   46.22    Outer_Syntax.command @{command_spec "print_translation"}
   46.23      "install print translation functions"
   46.24 -    (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
   46.25 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
   46.26  
   46.27  val _ =
   46.28    Outer_Syntax.command @{command_spec "typed_print_translation"}
   46.29      "install typed print translation functions"
   46.30 -    (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
   46.31 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
   46.32  
   46.33  val _ =
   46.34    Outer_Syntax.command @{command_spec "print_ast_translation"}
   46.35      "install print ast translation functions"
   46.36 -    (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   46.37 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   46.38  
   46.39  
   46.40  (* oracles *)
    47.1 --- a/src/Pure/Pure.thy	Sat May 25 15:44:29 2013 +0200
    47.2 +++ b/src/Pure/Pure.thy	Sat May 25 18:30:38 2013 +0200
    47.3 @@ -8,7 +8,7 @@
    47.4    keywords
    47.5      "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
    47.6      "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
    47.7 -    "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"
    47.8 +    "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes"
    47.9      "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
   47.10      "identifier" "if" "imports" "in" "includes" "infix" "infixl"
   47.11      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
    48.1 --- a/src/Pure/Syntax/local_syntax.ML	Sat May 25 15:44:29 2013 +0200
    48.2 +++ b/src/Pure/Syntax/local_syntax.ML	Sat May 25 18:30:38 2013 +0200
    48.3 @@ -59,11 +59,10 @@
    48.4        | update_gram ((false, add, m), decls) =
    48.5            Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    48.6  
    48.7 -    val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
    48.8      val local_syntax = thy_syntax
    48.9        |> Syntax.update_trfuns
   48.10 -          (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs,
   48.11 -           map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs')
   48.12 +          ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)],
   48.13 +           [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)])
   48.14        |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   48.15    in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
   48.16  
    49.1 --- a/src/Pure/Syntax/mixfix.ML	Sat May 25 15:44:29 2013 +0200
    49.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat May 25 18:30:38 2013 +0200
    49.3 @@ -145,10 +145,10 @@
    49.4      val mfix = maps mfix_of const_decls;
    49.5      val binders = map_filter binder const_decls;
    49.6      val binder_trs = binders
    49.7 -      |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
    49.8 +      |> map (Syntax_Ext.stamp_trfun binder_stamp o Syntax_Trans.mk_binder_tr);
    49.9      val binder_trs' = binders
   49.10        |> map (Syntax_Ext.stamp_trfun binder_stamp o
   49.11 -          apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   49.12 +          apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
   49.13  
   49.14      val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
   49.15    in
    50.1 --- a/src/Pure/Syntax/syntax.ML	Sat May 25 15:44:29 2013 +0200
    50.2 +++ b/src/Pure/Syntax/syntax.ML	Sat May 25 18:30:38 2013 +0200
    50.3 @@ -103,11 +103,6 @@
    50.4      Parse_Print_Rule of 'a * 'a
    50.5    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    50.6    val update_trfuns:
    50.7 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    50.8 -    (string * ((term list -> term) * stamp)) list *
    50.9 -    (string * ((typ -> term list -> term) * stamp)) list *
   50.10 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   50.11 -  val update_advanced_trfuns:
   50.12      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   50.13      (string * ((Proof.context -> term list -> term) * stamp)) list *
   50.14      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   50.15 @@ -651,10 +646,7 @@
   50.16  
   50.17  (** modify syntax **)
   50.18  
   50.19 -fun ext_syntax f decls = update_syntax mode_default (f decls);
   50.20 -
   50.21 -val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns;
   50.22 -val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns;
   50.23 +val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
   50.24  
   50.25  fun update_type_gram add prmode decls =
   50.26    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
   50.27 @@ -662,7 +654,7 @@
   50.28  fun update_const_gram add is_logtype prmode decls =
   50.29    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
   50.30  
   50.31 -val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
   50.32 +val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
   50.33  val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
   50.34  
   50.35  
    51.1 --- a/src/Pure/Syntax/syntax_ext.ML	Sat May 25 15:44:29 2013 +0200
    51.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Sat May 25 18:30:38 2013 +0200
    51.3 @@ -45,11 +45,6 @@
    51.4      (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    51.5    val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    51.6    val syn_ext_trfuns:
    51.7 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    51.8 -    (string * ((term list -> term) * stamp)) list *
    51.9 -    (string * ((typ -> term list -> term) * stamp)) list *
   51.10 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   51.11 -  val syn_ext_advanced_trfuns:
   51.12      (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   51.13      (string * ((Proof.context -> term list -> term) * stamp)) list *
   51.14      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   51.15 @@ -319,12 +314,7 @@
   51.16  val syn_ext = syn_ext' (K false);
   51.17  
   51.18  fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
   51.19 -fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
   51.20 -
   51.21 -fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
   51.22 -  let fun simple (name, (f, s)) = (name, (K f, s)) in
   51.23 -    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
   51.24 -  end;
   51.25 +fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
   51.26  
   51.27  fun stamp_trfun s (c, f) = (c, (f, s));
   51.28  fun mk_trfun tr = stamp_trfun (stamp ()) tr;
    52.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat May 25 15:44:29 2013 +0200
    52.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat May 25 18:30:38 2013 +0200
    52.3 @@ -751,10 +751,10 @@
    52.4  (* setup translations *)
    52.5  
    52.6  val _ = Context.>> (Context.map_theory
    52.7 - (Sign.add_advanced_trfuns
    52.8 -  ([("_context_const", const_ast_tr true),
    52.9 -    ("_context_xconst", const_ast_tr false)], [], [], []) #>
   52.10 -  Sign.add_advanced_trfunsT
   52.11 + (Sign.parse_ast_translation
   52.12 +   [("_context_const", const_ast_tr true),
   52.13 +    ("_context_xconst", const_ast_tr false)] #>
   52.14 +  Sign.typed_print_translation
   52.15     [("_type_prop", type_prop_tr'),
   52.16      ("\\<^const>TYPE", type_tr'),
   52.17      ("_type_constraint_", type_constraint_tr')]));
    53.1 --- a/src/Pure/Syntax/syntax_trans.ML	Sat May 25 15:44:29 2013 +0200
    53.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Sat May 25 18:30:38 2013 +0200
    53.3 @@ -19,12 +19,13 @@
    53.4    val no_type_bracketsN: string
    53.5    val no_type_brackets: unit -> bool
    53.6    val abs_tr: term list -> term
    53.7 -  val mk_binder_tr: string * string -> string * (term list -> term)
    53.8 +  val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
    53.9    val antiquote_tr: string -> term -> term
   53.10    val quote_tr: string -> term -> term
   53.11 -  val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
   53.12 -  val non_typed_tr': (term list -> term) -> typ -> term list -> term
   53.13 -  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
   53.14 +  val quote_antiquote_tr: string -> string -> string ->
   53.15 +    string * (Proof.context -> term list -> term)
   53.16 +  val non_typed_tr': (Proof.context -> term list -> term) ->
   53.17 +    Proof.context -> typ -> term list -> term
   53.18    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   53.19    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   53.20    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   53.21 @@ -35,27 +36,23 @@
   53.22    val abs_tr': Proof.context -> term -> term
   53.23    val atomic_abs_tr': string * typ * term -> term * term
   53.24    val const_abs_tr': term -> term
   53.25 -  val mk_binder_tr': string * string -> string * (term list -> term)
   53.26 -  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   53.27 -  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
   53.28 +  val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
   53.29 +  val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
   53.30 +  val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
   53.31    val prop_tr': term -> term
   53.32    val variant_abs: string * typ * term -> string * term
   53.33    val variant_abs': string * typ * term -> string * term
   53.34    val dependent_tr': string * string -> term list -> term
   53.35    val antiquote_tr': string -> term -> term
   53.36    val quote_tr': string -> term -> term
   53.37 -  val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
   53.38 +  val quote_antiquote_tr': string -> string -> string ->
   53.39 +    string * (Proof.context -> term list -> term)
   53.40    val update_name_tr': term -> term
   53.41 -  val pure_trfuns:
   53.42 -    (string * (Ast.ast list -> Ast.ast)) list *
   53.43 -    (string * (term list -> term)) list *
   53.44 -    (string * (term list -> term)) list *
   53.45 -    (string * (Ast.ast list -> Ast.ast)) list
   53.46 -  val struct_trfuns: string list ->
   53.47 -    (string * (Ast.ast list -> Ast.ast)) list *
   53.48 -    (string * (term list -> term)) list *
   53.49 -    (string * (typ -> term list -> term)) list *
   53.50 -    (string * (Ast.ast list -> Ast.ast)) list
   53.51 +  val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   53.52 +  val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
   53.53 +  val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   53.54 +  val struct_tr: string list -> string * (Proof.context -> term list -> term)
   53.55 +  val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
   53.56  end;
   53.57  
   53.58  structure Syntax_Trans: SYNTAX_TRANS =
   53.59 @@ -152,7 +149,7 @@
   53.60            let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
   53.61            in Syntax.const name $ abs end
   53.62        | binder_tr ts = err ts;
   53.63 -  in (syn, binder_tr) end;
   53.64 +  in (syn, fn _ => binder_tr) end;
   53.65  
   53.66  
   53.67  (* type propositions *)
   53.68 @@ -214,7 +211,7 @@
   53.69    let
   53.70      fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
   53.71        | tr ts = raise TERM ("quote_tr", ts);
   53.72 -  in (quoteN, tr) end;
   53.73 +  in (quoteN, fn _ => tr) end;
   53.74  
   53.75  
   53.76  (* corresponding updates *)
   53.77 @@ -246,12 +243,13 @@
   53.78  fun index_tr [t] = t
   53.79    | index_tr ts = raise TERM ("index_tr", ts);
   53.80  
   53.81 -fun the_struct [] = error "Illegal reference to implicit structure"
   53.82 -  | the_struct (x :: _) = x;
   53.83 -
   53.84 -fun struct_tr structs [Const ("_indexdefault", _)] =
   53.85 -      Syntax.const (Lexicon.mark_fixed (the_struct structs))
   53.86 -  | struct_tr _ ts = raise TERM ("struct_tr", ts);
   53.87 +fun struct_tr structs =
   53.88 +  ("_struct", fn _ =>
   53.89 +    (fn [Const ("_indexdefault", _)] =>
   53.90 +        (case structs of
   53.91 +          x :: _ => Syntax.const (Lexicon.mark_fixed x)
   53.92 +        | _ => error "Illegal reference to implicit structure")
   53.93 +      | ts => raise TERM ("struct_tr", ts)));
   53.94  
   53.95  
   53.96  
   53.97 @@ -259,8 +257,7 @@
   53.98  
   53.99  (* types *)
  53.100  
  53.101 -fun non_typed_tr' f _ ts = f ts;
  53.102 -fun non_typed_tr'' f x _ ts = f x ts;
  53.103 +fun non_typed_tr' f ctxt _ ts = f ctxt ts;
  53.104  
  53.105  
  53.106  (* type syntax *)
  53.107 @@ -366,13 +363,13 @@
  53.108  
  53.109      fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
  53.110        | binder_tr' [] = raise Match;
  53.111 -  in (name, binder_tr') end;
  53.112 +  in (name, fn _ => binder_tr') end;
  53.113  
  53.114 -fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
  53.115 +fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
  53.116    let val (x, t) = atomic_abs_tr' abs
  53.117    in list_comb (Syntax.const syn $ x $ t, ts) end);
  53.118  
  53.119 -fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
  53.120 +fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
  53.121    let val (x, t) = atomic_abs_tr' abs
  53.122    in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
  53.123  
  53.124 @@ -464,7 +461,7 @@
  53.125    let
  53.126      fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
  53.127        | tr' _ = raise Match;
  53.128 -  in (name, tr') end;
  53.129 +  in (name, fn _ => tr') end;
  53.130  
  53.131  
  53.132  (* corresponding updates *)
  53.133 @@ -494,48 +491,51 @@
  53.134  fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
  53.135    | index_ast_tr' _ = raise Match;
  53.136  
  53.137 -fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =
  53.138 -      Ast.Appl [Ast.Constant "_free",
  53.139 -        Ast.Variable (the_struct structs handle ERROR _ => raise Match)]
  53.140 -  | struct_ast_tr' _ _ = raise Match;
  53.141 +fun struct_ast_tr' structs =
  53.142 +  ("_struct", fn _ =>
  53.143 +    (fn [Ast.Constant "_indexdefault"] =>
  53.144 +        (case structs of
  53.145 +          x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
  53.146 +        | _ => raise Match)
  53.147 +      | _ => raise Match));
  53.148  
  53.149  
  53.150  
  53.151  (** Pure translations **)
  53.152  
  53.153 -val pure_trfuns =
  53.154 -  ([("_strip_positions", strip_positions_ast_tr),
  53.155 -    ("_constify", constify_ast_tr),
  53.156 -    ("_tapp", tapp_ast_tr),
  53.157 -    ("_tappl", tappl_ast_tr),
  53.158 -    ("_bracket", bracket_ast_tr),
  53.159 -    ("_appl", appl_ast_tr),
  53.160 -    ("_applC", applC_ast_tr),
  53.161 -    ("_lambda", lambda_ast_tr),
  53.162 -    ("_idtyp", idtyp_ast_tr),
  53.163 -    ("_idtypdummy", idtypdummy_ast_tr),
  53.164 -    ("_bigimpl", bigimpl_ast_tr),
  53.165 -    ("_indexdefault", indexdefault_ast_tr),
  53.166 -    ("_indexvar", indexvar_ast_tr),
  53.167 -    ("_struct", struct_ast_tr)],
  53.168 -   [("_abs", abs_tr),
  53.169 -    ("_aprop", aprop_tr),
  53.170 -    ("_ofclass", ofclass_tr),
  53.171 -    ("_sort_constraint", sort_constraint_tr),
  53.172 -    ("_TYPE", type_tr),
  53.173 -    ("_DDDOT", dddot_tr),
  53.174 -    ("_update_name", update_name_tr),
  53.175 -    ("_index", index_tr)],
  53.176 -   ([]: (string * (term list -> term)) list),
  53.177 -   [("\\<^type>fun", fun_ast_tr'),
  53.178 -    ("_abs", abs_ast_tr'),
  53.179 -    ("_idts", idtyp_ast_tr' "_idts"),
  53.180 -    ("_pttrns", idtyp_ast_tr' "_pttrns"),
  53.181 -    ("\\<^const>==>", impl_ast_tr'),
  53.182 -    ("_index", index_ast_tr')]);
  53.183 +val pure_parse_ast_translation =
  53.184 + [("_strip_positions", fn _ => strip_positions_ast_tr),
  53.185 +  ("_constify", fn _ => constify_ast_tr),
  53.186 +  ("_tapp", fn _ => tapp_ast_tr),
  53.187 +  ("_tappl", fn _ => tappl_ast_tr),
  53.188 +  ("_bracket", fn _ => bracket_ast_tr),
  53.189 +  ("_appl", fn _ => appl_ast_tr),
  53.190 +  ("_applC", fn _ => applC_ast_tr),
  53.191 +  ("_lambda", fn _ => lambda_ast_tr),
  53.192 +  ("_idtyp", fn _ => idtyp_ast_tr),
  53.193 +  ("_idtypdummy", fn _ => idtypdummy_ast_tr),
  53.194 +  ("_bigimpl", fn _ => bigimpl_ast_tr),
  53.195 +  ("_indexdefault", fn _ => indexdefault_ast_tr),
  53.196 +  ("_indexvar", fn _ => indexvar_ast_tr),
  53.197 +  ("_struct", fn _ => struct_ast_tr)];
  53.198  
  53.199 -fun struct_trfuns structs =
  53.200 -  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
  53.201 +val pure_parse_translation =
  53.202 + [("_abs", fn _ => abs_tr),
  53.203 +  ("_aprop", fn _ => aprop_tr),
  53.204 +  ("_ofclass", fn _ => ofclass_tr),
  53.205 +  ("_sort_constraint", fn _ => sort_constraint_tr),
  53.206 +  ("_TYPE", fn _ => type_tr),
  53.207 +  ("_DDDOT", fn _ => dddot_tr),
  53.208 +  ("_update_name", fn _ => update_name_tr),
  53.209 +  ("_index", fn _ => index_tr)];
  53.210 +
  53.211 +val pure_print_ast_translation =
  53.212 + [("\\<^type>fun", fn _ => fun_ast_tr'),
  53.213 +  ("_abs", fn _ => abs_ast_tr'),
  53.214 +  ("_idts", fn _ => idtyp_ast_tr' "_idts"),
  53.215 +  ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
  53.216 +  ("\\<^const>==>", fn _ => impl_ast_tr'),
  53.217 +  ("_index", fn _ => index_ast_tr')];
  53.218  
  53.219  end;
  53.220  
    54.1 --- a/src/Pure/pure_thy.ML	Sat May 25 15:44:29 2013 +0200
    54.2 +++ b/src/Pure/pure_thy.ML	Sat May 25 18:30:38 2013 +0200
    54.3 @@ -189,7 +189,9 @@
    54.4    #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
    54.5    #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
    54.6    #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
    54.7 -  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
    54.8 +  #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
    54.9 +  #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   54.10 +  #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
   54.11    #> Sign.local_path
   54.12    #> Sign.add_consts_i
   54.13     [(Binding.name "term", typ "'a => prop", NoSyn),
    55.1 --- a/src/Pure/sign.ML	Sat May 25 15:44:29 2013 +0200
    55.2 +++ b/src/Pure/sign.ML	Sat May 25 18:30:38 2013 +0200
    55.3 @@ -87,19 +87,16 @@
    55.4    val primitive_class: binding * class list -> theory -> theory
    55.5    val primitive_classrel: class * class -> theory -> theory
    55.6    val primitive_arity: arity -> theory -> theory
    55.7 -  val add_trfuns:
    55.8 -    (string * (Ast.ast list -> Ast.ast)) list *
    55.9 -    (string * (term list -> term)) list *
   55.10 -    (string * (term list -> term)) list *
   55.11 -    (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
   55.12 -  val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
   55.13 -  val add_advanced_trfuns:
   55.14 -    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
   55.15 -    (string * (Proof.context -> term list -> term)) list *
   55.16 -    (string * (Proof.context -> term list -> term)) list *
   55.17 +  val parse_ast_translation:
   55.18      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   55.19 -  val add_advanced_trfunsT:
   55.20 +  val parse_translation:
   55.21 +    (string * (Proof.context -> term list -> term)) list -> theory -> theory
   55.22 +  val print_translation:
   55.23 +    (string * (Proof.context -> term list -> term)) list -> theory -> theory
   55.24 +  val typed_print_translation:
   55.25      (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
   55.26 +  val print_ast_translation:
   55.27 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   55.28    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   55.29    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   55.30    val new_group: theory -> theory
   55.31 @@ -466,17 +463,14 @@
   55.32  
   55.33  fun mk trs = map Syntax_Ext.mk_trfun trs;
   55.34  
   55.35 -fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) =
   55.36 -  map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));
   55.37 -
   55.38 -fun gen_add_trfunsT ext tr's = map_syn (ext ([], [], mk tr's, []));
   55.39 -
   55.40  in
   55.41  
   55.42 -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
   55.43 -val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
   55.44 -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
   55.45 -val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
   55.46 +fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
   55.47 +fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
   55.48 +fun print_translation tr's =
   55.49 +  map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
   55.50 +fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
   55.51 +fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
   55.52  
   55.53  end;
   55.54  
    56.1 --- a/src/Sequents/ILL.thy	Sat May 25 15:44:29 2013 +0200
    56.2 +++ b/src/Sequents/ILL.thy	Sat May 25 18:30:38 2013 +0200
    56.3 @@ -36,15 +36,15 @@
    56.4    "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    56.5  
    56.6  parse_translation {*
    56.7 -  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
    56.8 -   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
    56.9 -   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
   56.10 +  [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
   56.11 +   (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
   56.12 +   (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
   56.13  *}
   56.14  
   56.15  print_translation {*
   56.16 -  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
   56.17 -   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
   56.18 -   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
   56.19 +  [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
   56.20 +   (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
   56.21 +   (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
   56.22  *}
   56.23  
   56.24  defs
    57.1 --- a/src/Sequents/LK0.thy	Sat May 25 15:44:29 2013 +0200
    57.2 +++ b/src/Sequents/LK0.thy	Sat May 25 18:30:38 2013 +0200
    57.3 @@ -34,8 +34,8 @@
    57.4  syntax
    57.5   "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    57.6  
    57.7 -parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
    57.8 -print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
    57.9 +parse_translation {* [(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))] *}
   57.10 +print_translation {* [(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))] *}
   57.11  
   57.12  abbreviation
   57.13    not_equal  (infixl "~=" 50) where
    58.1 --- a/src/Sequents/Modal0.thy	Sat May 25 15:44:29 2013 +0200
    58.2 +++ b/src/Sequents/Modal0.thy	Sat May 25 18:30:38 2013 +0200
    58.3 @@ -27,13 +27,13 @@
    58.4  *}
    58.5  
    58.6  parse_translation {*
    58.7 - [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
    58.8 -  (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
    58.9 + [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
   58.10 +  (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
   58.11  *}
   58.12  
   58.13  print_translation {*
   58.14 - [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
   58.15 -  (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
   58.16 + [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
   58.17 +  (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
   58.18  *}
   58.19  
   58.20  defs
    59.1 --- a/src/Sequents/S43.thy	Sat May 25 15:44:29 2013 +0200
    59.2 +++ b/src/Sequents/S43.thy	Sat May 25 18:30:38 2013 +0200
    59.3 @@ -21,7 +21,7 @@
    59.4      val tr  = seq_tr;
    59.5      fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
    59.6        Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
    59.7 -  in [(@{syntax_const "_S43pi"}, s43pi_tr)] end
    59.8 +  in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
    59.9  *}
   59.10  
   59.11  print_translation {*
   59.12 @@ -29,7 +29,7 @@
   59.13    val tr' = seq_tr';
   59.14    fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
   59.15      Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
   59.16 -in [(@{const_syntax S43pi}, s43pi_tr')] end
   59.17 +in [(@{const_syntax S43pi}, K s43pi_tr')] end
   59.18  *}
   59.19  
   59.20  axiomatization where
    60.1 --- a/src/Sequents/Sequents.thy	Sat May 25 15:44:29 2013 +0200
    60.2 +++ b/src/Sequents/Sequents.thy	Sat May 25 18:30:38 2013 +0200
    60.3 @@ -139,7 +139,7 @@
    60.4  fun side_tr [s1] = seq_tr s1;
    60.5  *}
    60.6  
    60.7 -parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
    60.8 +parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
    60.9  
   60.10  ML_file "prover.ML"
   60.11  
    61.1 --- a/src/ZF/Tools/inductive_package.ML	Sat May 25 15:44:29 2013 +0200
    61.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat May 25 18:30:38 2013 +0200
    61.3 @@ -260,8 +260,8 @@
    61.4        THEN (PRIMITIVE (fold_rule part_rec_defs));
    61.5  
    61.6    (*Elimination*)
    61.7 -  val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1)
    61.8 -                 (unfold RS Ind_Syntax.equals_CollectD)
    61.9 +  val elim =
   61.10 +    rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (unfold RS Ind_Syntax.equals_CollectD)
   61.11  
   61.12    (*Applies freeness of the given constructors, which *must* be unfolded by
   61.13        the given defs.  Cannot simply use the local con_defs because
    62.1 --- a/src/ZF/Tools/numeral_syntax.ML	Sat May 25 15:44:29 2013 +0200
    62.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Sat May 25 18:30:38 2013 +0200
    62.3 @@ -79,6 +79,7 @@
    62.4  
    62.5  
    62.6  val setup =
    62.7 - Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [(@{const_syntax integ_of}, int_tr')], []);
    62.8 + Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #>
    62.9 + Sign.print_translation [(@{const_syntax integ_of}, K int_tr')];
   62.10  
   62.11  end;