explicit structure Syntax_Trans;
authorwenzelm
Fri Apr 08 13:31:16 2011 +0200 (2011-04-08)
changeset 42284326f57825e1a
parent 42283 25d9d836ed9c
child 42285 8d91a85b6d91
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
NEWS
src/CCL/Term.thy
src/CCL/Type.thy
src/Cube/Cube.thy
src/FOLP/simp.ML
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattice.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Hoare_Parallel/OG_Syntax.thy
src/HOL/Hoare_Parallel/Quote_Antiquote.thy
src/HOL/Hoare_Parallel/RG_Syntax.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Library/reflection.ML
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/record.ML
src/HOL/ex/Antiquote.thy
src/Pure/IsaMakefile
src/Pure/Isar/attrib.ML
src/Pure/Isar/obtain.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ROOT.ML
src/Pure/Syntax/local_syntax.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/Thy/thy_output.ML
src/Pure/primitive_defs.ML
src/Pure/pure_thy.ML
src/Pure/raw_simplifier.ML
src/Pure/sign.ML
src/Pure/type_infer.ML
src/Tools/Code/code_thingol.ML
src/Tools/induct.ML
src/Tools/misc_legacy.ML
src/Tools/subtyping.ML
     1.1 --- a/NEWS	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/NEWS	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -93,9 +93,10 @@
     1.4  be disabled via the configuration option Syntax.positions, which is
     1.5  called "syntax_positions" in Isar attribute syntax.
     1.6  
     1.7 -* Discontinued special treatment of structure Ast: no pervasive
     1.8 -content, no inclusion in structure Syntax.  INCOMPATIBILITY, refer to
     1.9 -qualified names like Ast.Constant etc.
    1.10 +* Discontinued special treatment of various ML structures of inner
    1.11 +syntax, such as structure Ast: no pervasive content, no inclusion in
    1.12 +structure Syntax.  INCOMPATIBILITY, refer to qualified names like
    1.13 +Ast.Constant etc.
    1.14  
    1.15  * Typed print translation: discontinued show_sorts argument, which is
    1.16  already available via context of "advanced" translation.
     2.1 --- a/src/CCL/Term.thy	Fri Apr 08 11:39:45 2011 +0200
     2.2 +++ b/src/CCL/Term.thy	Fri Apr 08 13:31:16 2011 +0200
     2.3 @@ -56,11 +56,11 @@
     2.4  (** Quantifier translations: variable binding **)
     2.5  
     2.6  (* FIXME does not handle "_idtdummy" *)
     2.7 -(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
     2.8 +(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
     2.9  
    2.10  fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
    2.11  fun let_tr' [a,Abs(id,T,b)] =
    2.12 -     let val (id',b') = variant_abs(id,T,b)
    2.13 +     let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
    2.14       in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
    2.15  
    2.16  fun letrec_tr [Free(f,S),Free(x,T),a,b] =
    2.17 @@ -72,23 +72,23 @@
    2.18          absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
    2.19  
    2.20  fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
    2.21 -     let val (f',b')  = variant_abs(ff,SS,b)
    2.22 -         val (_,a'') = variant_abs(f,S,a)
    2.23 -         val (x',a')  = variant_abs(x,T,a'')
    2.24 +     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
    2.25 +         val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
    2.26 +         val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
    2.27       in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
    2.28  fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
    2.29 -     let val (f',b') = variant_abs(ff,SS,b)
    2.30 -         val ( _,a1) = variant_abs(f,S,a)
    2.31 -         val (y',a2) = variant_abs(y,U,a1)
    2.32 -         val (x',a') = variant_abs(x,T,a2)
    2.33 +     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
    2.34 +         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
    2.35 +         val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
    2.36 +         val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
    2.37       in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
    2.38        end;
    2.39  fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
    2.40 -     let val (f',b') = variant_abs(ff,SS,b)
    2.41 -         val ( _,a1) = variant_abs(f,S,a)
    2.42 -         val (z',a2) = variant_abs(z,V,a1)
    2.43 -         val (y',a3) = variant_abs(y,U,a2)
    2.44 -         val (x',a') = variant_abs(x,T,a3)
    2.45 +     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
    2.46 +         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
    2.47 +         val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
    2.48 +         val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
    2.49 +         val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
    2.50       in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
    2.51        end;
    2.52  
     3.1 --- a/src/CCL/Type.thy	Fri Apr 08 11:39:45 2011 +0200
     3.2 +++ b/src/CCL/Type.thy	Fri Apr 08 13:31:16 2011 +0200
     3.3 @@ -46,8 +46,10 @@
     3.4    "{x: A. B}"   == "CONST Subtype(A, %x. B)"
     3.5  
     3.6  print_translation {*
     3.7 - [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
     3.8 -  (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
     3.9 + [(@{const_syntax Pi},
    3.10 +    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
    3.11 +  (@{const_syntax Sigma},
    3.12 +    Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
    3.13  *}
    3.14  
    3.15  defs
     4.1 --- a/src/Cube/Cube.thy	Fri Apr 08 11:39:45 2011 +0200
     4.2 +++ b/src/Cube/Cube.thy	Fri Apr 08 13:31:16 2011 +0200
     4.3 @@ -53,7 +53,8 @@
     4.4    "_arrow" :: "[term, term] => term"    (infixr "\<rightarrow>" 10)
     4.5  
     4.6  print_translation {*
     4.7 -  [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
     4.8 +  [(@{const_syntax Prod},
     4.9 +    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
    4.10  *}
    4.11  
    4.12  axioms
     5.1 --- a/src/FOLP/simp.ML	Fri Apr 08 11:39:45 2011 +0200
     5.2 +++ b/src/FOLP/simp.ML	Fri Apr 08 13:31:16 2011 +0200
     5.3 @@ -371,7 +371,7 @@
     5.4  (*Replace parameters by Free variables in P*)
     5.5  fun variants_abs ([],P) = P
     5.6    | variants_abs ((a,T)::aTs, P) =
     5.7 -      variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
     5.8 +      variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P)));
     5.9  
    5.10  (*Select subgoal i from proof state; substitute parameters, for printing*)
    5.11  fun prepare_goal i st =
     6.1 --- a/src/HOL/Big_Operators.thy	Fri Apr 08 11:39:45 2011 +0200
     6.2 +++ b/src/HOL/Big_Operators.thy	Fri Apr 08 13:31:16 2011 +0200
     6.3 @@ -86,10 +86,10 @@
     6.4          if x <> y then raise Match
     6.5          else
     6.6            let
     6.7 -            val x' = Syntax.mark_bound x;
     6.8 +            val x' = Syntax_Trans.mark_bound x;
     6.9              val t' = subst_bound (x', t);
    6.10              val P' = subst_bound (x', P);
    6.11 -          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
    6.12 +          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
    6.13      | setsum_tr' _ = raise Match;
    6.14  in [(@{const_syntax setsum}, setsum_tr')] end
    6.15  *}
     7.1 --- a/src/HOL/Complete_Lattice.thy	Fri Apr 08 11:39:45 2011 +0200
     7.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Apr 08 13:31:16 2011 +0200
     7.3 @@ -159,8 +159,8 @@
     7.4    "SUP x:A. B"   == "CONST SUPR A (%x. B)"
     7.5  
     7.6  print_translation {*
     7.7 -  [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
     7.8 -    Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
     7.9 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
    7.10 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
    7.11  *} -- {* to avoid eta-contraction of body *}
    7.12  
    7.13  context complete_lattice
    7.14 @@ -409,7 +409,7 @@
    7.15    "INT x:A. B"  == "CONST INTER A (%x. B)"
    7.16  
    7.17  print_translation {*
    7.18 -  [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    7.19 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    7.20  *} -- {* to avoid eta-contraction of body *}
    7.21  
    7.22  lemma INTER_eq_Inter_image:
    7.23 @@ -612,7 +612,7 @@
    7.24  *}
    7.25  
    7.26  print_translation {*
    7.27 -  [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
    7.28 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
    7.29  *} -- {* to avoid eta-contraction of body *}
    7.30  
    7.31  lemma UNION_eq_Union_image:
     8.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 08 11:39:45 2011 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 08 13:31:16 2011 +0200
     8.3 @@ -1924,12 +1924,12 @@
     8.4        @{code NOT} (fm_of_term ps vs t')
     8.5    | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
     8.6        let
     8.7 -        val (xn', p') = variant_abs (xn, xT, p);
     8.8 +        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
     8.9          val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
    8.10        in @{code E} (fm_of_term ps vs' p) end
    8.11    | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
    8.12        let
    8.13 -        val (xn', p') = variant_abs (xn, xT, p);
    8.14 +        val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
    8.15          val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
    8.16        in @{code A} (fm_of_term ps vs' p) end
    8.17    | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
    8.18 @@ -1988,7 +1988,7 @@
    8.19          else insert (op aconv) t acc
    8.20      | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a  
    8.21          else insert (op aconv) t acc
    8.22 -    | Abs p => term_bools acc (snd (variant_abs p))
    8.23 +    | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
    8.24      | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
    8.25    end;
    8.26  
     9.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 08 11:39:45 2011 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 08 13:31:16 2011 +0200
     9.3 @@ -2939,13 +2939,13 @@
     9.4    | Const(@{const_name Orderings.less_eq},_)$p$q => 
     9.5          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
     9.6    | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
     9.7 -     let val (xn', p') =  variant_abs (xn,xT,p)
     9.8 +     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
     9.9           val x = Free(xn',xT)
    9.10           fun incr i = i + 1
    9.11           val m0 = (x,0):: (map (apsnd incr) m)
    9.12        in @{code E} (fm_of_term m0 m' p') end
    9.13    | Const(@{const_name All},_)$Abs(xn,xT,p) => 
    9.14 -     let val (xn', p') =  variant_abs (xn,xT,p)
    9.15 +     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
    9.16           val x = Free(xn',xT)
    9.17           fun incr i = i + 1
    9.18           val m0 = (x,0):: (map (apsnd incr) m)
    10.1 --- a/src/HOL/HOL.thy	Fri Apr 08 11:39:45 2011 +0200
    10.2 +++ b/src/HOL/HOL.thy	Fri Apr 08 13:31:16 2011 +0200
    10.3 @@ -130,7 +130,7 @@
    10.4  
    10.5  print_translation {*
    10.6    [(@{const_syntax The}, fn [Abs abs] =>
    10.7 -      let val (x, t) = atomic_abs_tr' abs
    10.8 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    10.9        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
   10.10  *}  -- {* To avoid eta-contraction of body *}
   10.11  
    11.1 --- a/src/HOL/HOLCF/Cfun.thy	Fri Apr 08 11:39:45 2011 +0200
    11.2 +++ b/src/HOL/HOLCF/Cfun.thy	Fri Apr 08 13:31:16 2011 +0200
    11.3 @@ -34,12 +34,12 @@
    11.4  
    11.5  parse_translation {*
    11.6  (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
    11.7 -  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
    11.8 +  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
    11.9  *}
   11.10  
   11.11  print_translation {*
   11.12    [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
   11.13 -      let val (x, t) = atomic_abs_tr' abs
   11.14 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
   11.15        in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
   11.16  *}  -- {* To avoid eta-contraction of body *}
   11.17  
    12.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 11:39:45 2011 +0200
    12.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 13:31:16 2011 +0200
    12.3 @@ -132,7 +132,7 @@
    12.4  (* rewrite (_pat x) => (succeed) *)
    12.5  (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
    12.6   [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
    12.7 -  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
    12.8 +  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
    12.9  *}
   12.10  
   12.11  text {* Printing Case expressions *}
   12.12 @@ -154,7 +154,7 @@
   12.13              val abs =
   12.14                case t of Abs abs => abs
   12.15                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   12.16 -            val (x, t') = atomic_abs_tr' abs;
   12.17 +            val (x, t') = Syntax_Trans.atomic_abs_tr' abs;
   12.18            in (Syntax.const @{syntax_const "_variable"} $ x, t') end
   12.19      |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   12.20  
    13.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Apr 08 11:39:45 2011 +0200
    13.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Apr 08 13:31:16 2011 +0200
    13.3 @@ -26,7 +26,7 @@
    13.4  
    13.5  print_translation {*
    13.6    [(@{const_syntax Eps}, fn [Abs abs] =>
    13.7 -      let val (x, t) = atomic_abs_tr' abs
    13.8 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    13.9        in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
   13.10  *} -- {* to avoid eta-contraction of body *}
   13.11  
    14.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Fri Apr 08 11:39:45 2011 +0200
    14.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Fri Apr 08 13:31:16 2011 +0200
    14.3 @@ -26,9 +26,9 @@
    14.4      (SOME x, SOME y) => x = y
    14.5    | _ => false);
    14.6  
    14.7 -fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
    14.8 +fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
    14.9    | mk_abstuple (x :: xs) body =
   14.10 -      Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
   14.11 +      Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
   14.12  
   14.13  fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   14.14    | mk_fbody x e (y :: xs) =
    15.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 11:39:45 2011 +0200
    15.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 13:31:16 2011 +0200
    15.3 @@ -76,11 +76,11 @@
    15.4  print_translation {*
    15.5    let
    15.6      fun quote_tr' f (t :: ts) =
    15.7 -          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
    15.8 +          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
    15.9        | quote_tr' _ _ = raise Match;
   15.10  
   15.11      fun annquote_tr' f (r :: t :: ts) =
   15.12 -          Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   15.13 +          Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
   15.14        | annquote_tr' _ _ = raise Match;
   15.15  
   15.16      val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   15.17 @@ -94,13 +94,13 @@
   15.18        | annbexp_tr' _ _ = raise Match;
   15.19  
   15.20      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   15.21 -          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
   15.22 -            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
   15.23 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
   15.24 +            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   15.25        | assign_tr' _ = raise Match;
   15.26  
   15.27      fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
   15.28 -          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
   15.29 -            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
   15.30 +          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
   15.31 +            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   15.32        | annassign_tr' _ = raise Match;
   15.33  
   15.34      fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
    16.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
    16.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
    16.3 @@ -16,7 +16,7 @@
    16.4  
    16.5  parse_translation {*
    16.6    let
    16.7 -    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
    16.8 +    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
    16.9        | quote_tr ts = raise TERM ("quote_tr", ts);
   16.10    in [(@{syntax_const "_quote"}, quote_tr)] end
   16.11  *}
    17.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Apr 08 11:39:45 2011 +0200
    17.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Fri Apr 08 13:31:16 2011 +0200
    17.3 @@ -58,7 +58,7 @@
    17.4  print_translation {*
    17.5    let
    17.6      fun quote_tr' f (t :: ts) =
    17.7 -          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
    17.8 +          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
    17.9        | quote_tr' _ _ = raise Match;
   17.10  
   17.11      val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   17.12 @@ -68,8 +68,8 @@
   17.13        | bexp_tr' _ _ = raise Match;
   17.14  
   17.15      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   17.16 -          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
   17.17 -            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
   17.18 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
   17.19 +            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   17.20        | assign_tr' _ = raise Match;
   17.21    in
   17.22     [(@{const_syntax Collect}, assert_tr'),
    18.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 11:39:45 2011 +0200
    18.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 13:31:16 2011 +0200
    18.3 @@ -185,8 +185,8 @@
    18.4    of the concrete syntactic representation of our Hoare language, the
    18.5    actual ``ML drivers'' is quite involved.  Just note that the we
    18.6    re-use the basic quote/antiquote translations as already defined in
    18.7 -  Isabelle/Pure (see \verb,Syntax.quote_tr, and
    18.8 -  \verb,Syntax.quote_tr',). *}
    18.9 +  Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
   18.10 +  @{ML Syntax_Trans.quote_tr'},). *}
   18.11  
   18.12  syntax
   18.13    "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
   18.14 @@ -215,7 +215,7 @@
   18.15  
   18.16  parse_translation {*
   18.17    let
   18.18 -    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
   18.19 +    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
   18.20        | quote_tr ts = raise TERM ("quote_tr", ts);
   18.21    in [(@{syntax_const "_quote"}, quote_tr)] end
   18.22  *}
   18.23 @@ -228,7 +228,7 @@
   18.24  print_translation {*
   18.25    let
   18.26      fun quote_tr' f (t :: ts) =
   18.27 -          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   18.28 +          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
   18.29        | quote_tr' _ _ = raise Match;
   18.30  
   18.31      val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   18.32 @@ -238,8 +238,8 @@
   18.33        | bexp_tr' _ _ = raise Match;
   18.34  
   18.35      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   18.36 -          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
   18.37 -            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
   18.38 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
   18.39 +            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   18.40        | assign_tr' _ = raise Match;
   18.41    in
   18.42     [(@{const_syntax Collect}, assert_tr'),
    19.1 --- a/src/HOL/Library/reflection.ML	Fri Apr 08 11:39:45 2011 +0200
    19.2 +++ b/src/HOL/Library/reflection.ML	Fri Apr 08 13:31:16 2011 +0200
    19.3 @@ -125,7 +125,7 @@
    19.4               Abs(xn,xT,ta) => (
    19.5                 let
    19.6                   val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
    19.7 -                 val (xn,ta) = variant_abs (xn,xT,ta)
    19.8 +                 val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta)  (* FIXME !? *)
    19.9                   val x = Free(xn,xT)
   19.10                   val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT)
   19.11                            of NONE => error "tryabsdecomp: Type not found in the Environement"
    20.1 --- a/src/HOL/Orderings.thy	Fri Apr 08 11:39:45 2011 +0200
    20.2 +++ b/src/HOL/Orderings.thy	Fri Apr 08 13:31:16 2011 +0200
    20.3 @@ -660,7 +660,7 @@
    20.4        Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
    20.5      | _ => false);
    20.6    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
    20.7 -  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
    20.8 +  fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
    20.9  
   20.10    fun tr' q = (q,
   20.11      fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
    21.1 --- a/src/HOL/Product_Type.thy	Fri Apr 08 11:39:45 2011 +0200
    21.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 08 13:31:16 2011 +0200
    21.3 @@ -199,8 +199,8 @@
    21.4    fun split_tr' [Abs (x, T, t as (Abs abs))] =
    21.5          (* split (%x y. t) => %(x,y) t *)
    21.6          let
    21.7 -          val (y, t') = atomic_abs_tr' abs;
    21.8 -          val (x', t'') = atomic_abs_tr' (x, T, t');
    21.9 +          val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
   21.10 +          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   21.11          in
   21.12            Syntax.const @{syntax_const "_abs"} $
   21.13              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   21.14 @@ -210,7 +210,7 @@
   21.15          let
   21.16            val Const (@{syntax_const "_abs"}, _) $
   21.17              (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
   21.18 -          val (x', t'') = atomic_abs_tr' (x, T, t');
   21.19 +          val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
   21.20          in
   21.21            Syntax.const @{syntax_const "_abs"} $
   21.22              (Syntax.const @{syntax_const "_pattern"} $ x' $
   21.23 @@ -221,7 +221,7 @@
   21.24          split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   21.25      | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   21.26          (* split (%pttrn z. t) => %(pttrn,z). t *)
   21.27 -        let val (z, t) = atomic_abs_tr' abs in
   21.28 +        let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
   21.29            Syntax.const @{syntax_const "_abs"} $
   21.30              (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   21.31          end
   21.32 @@ -239,8 +239,8 @@
   21.33          | _ =>
   21.34            let 
   21.35              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   21.36 -            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
   21.37 -            val (x', t'') = atomic_abs_tr' (x, xT, t');
   21.38 +            val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
   21.39 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
   21.40            in
   21.41              Syntax.const @{syntax_const "_abs"} $
   21.42                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   21.43 @@ -251,8 +251,9 @@
   21.44          | _ =>
   21.45            let
   21.46              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   21.47 -            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
   21.48 -            val (x', t'') = atomic_abs_tr' ("x", xT, t');
   21.49 +            val (y, t') =
   21.50 +              Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
   21.51 +            val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
   21.52            in
   21.53              Syntax.const @{syntax_const "_abs"} $
   21.54                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   21.55 @@ -276,10 +277,10 @@
   21.56      | _ => f ts;
   21.57    fun contract2 (Q,f) = (Q, contract Q f);
   21.58    val pairs =
   21.59 -    [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   21.60 -     Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
   21.61 -     Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
   21.62 -     Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
   21.63 +    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   21.64 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
   21.65 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
   21.66 +     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
   21.67  in map contract2 pairs end
   21.68  *}
   21.69  
    22.1 --- a/src/HOL/Set.thy	Fri Apr 08 11:39:45 2011 +0200
    22.2 +++ b/src/HOL/Set.thy	Fri Apr 08 13:31:16 2011 +0200
    22.3 @@ -246,7 +246,7 @@
    22.4  
    22.5    fun mk v v' c n P =
    22.6      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
    22.7 -    then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
    22.8 +    then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
    22.9  
   22.10    fun tr' q = (q,
   22.11          fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
   22.12 @@ -275,7 +275,7 @@
   22.13  
   22.14  parse_translation {*
   22.15    let
   22.16 -    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
   22.17 +    val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));
   22.18  
   22.19      fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
   22.20        | nvars _ = 1;
   22.21 @@ -291,13 +291,13 @@
   22.22  *}
   22.23  
   22.24  print_translation {*
   22.25 - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   22.26 -  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
   22.27 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   22.28 +  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
   22.29  *} -- {* to avoid eta-contraction of body *}
   22.30  
   22.31  print_translation {*
   22.32  let
   22.33 -  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
   22.34 +  val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
   22.35  
   22.36    fun setcompr_tr' [Abs (abs as (_, _, P))] =
   22.37      let
   22.38 @@ -315,7 +315,7 @@
   22.39        if check (P, 0) then tr' P
   22.40        else
   22.41          let
   22.42 -          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
   22.43 +          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
   22.44            val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
   22.45          in
   22.46            case t of
    23.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 11:39:45 2011 +0200
    23.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 13:31:16 2011 +0200
    23.3 @@ -454,12 +454,12 @@
    23.4        let val xs = Term.add_frees pat [] in
    23.5          Syntax.const @{syntax_const "_case1"} $
    23.6            map_aterms
    23.7 -            (fn Free p => Syntax.mark_boundT p
    23.8 +            (fn Free p => Syntax_Trans.mark_boundT p
    23.9                | Const (s, _) => Syntax.const (Syntax.mark_const s)
   23.10                | t => t) pat $
   23.11            map_aterms
   23.12              (fn x as Free (s, T) =>
   23.13 -                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
   23.14 +                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
   23.15                | t => t) rhs
   23.16        end;
   23.17    in
    24.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 08 11:39:45 2011 +0200
    24.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 08 13:31:16 2011 +0200
    24.3 @@ -579,13 +579,13 @@
    24.4                else insert (op aconv) t
    24.5      | f $ a => if skip orelse is_op f then add_bools a o add_bools f
    24.6                else insert (op aconv) t
    24.7 -    | Abs p => add_bools (snd (variant_abs p))
    24.8 +    | Abs p => add_bools (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
    24.9      | _ => if skip orelse is_op t then I else insert (op aconv) t
   24.10    end;
   24.11  
   24.12  fun descend vs (abs as (_, xT, _)) =
   24.13    let
   24.14 -    val (xn', p') = variant_abs abs;
   24.15 +    val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
   24.16    in ((xn', xT) :: vs, p') end;
   24.17  
   24.18  local structure Proc = Cooper_Procedure in
    25.1 --- a/src/HOL/Tools/record.ML	Fri Apr 08 11:39:45 2011 +0200
    25.2 +++ b/src/HOL/Tools/record.ML	Fri Apr 08 13:31:16 2011 +0200
    25.3 @@ -963,7 +963,7 @@
    25.4  fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
    25.5        (case dest_update ctxt c of
    25.6          SOME name =>
    25.7 -          (case try Syntax.const_abs_tr' k of
    25.8 +          (case try Syntax_Trans.const_abs_tr' k of
    25.9              SOME t =>
   25.10                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
   25.11                  (field_updates_tr' ctxt u)
    26.1 --- a/src/HOL/ex/Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
    26.2 +++ b/src/HOL/ex/Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
    26.3 @@ -25,11 +25,13 @@
    26.4    where "Expr exp env = exp env"
    26.5  
    26.6  parse_translation {*
    26.7 -  [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
    26.8 +  [Syntax_Trans.quote_antiquote_tr
    26.9 +    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
   26.10  *}
   26.11  
   26.12  print_translation {*
   26.13 -  [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
   26.14 +  [Syntax_Trans.quote_antiquote_tr'
   26.15 +    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
   26.16  *}
   26.17  
   26.18  term "EXPR (a + b + c)"
    27.1 --- a/src/Pure/IsaMakefile	Fri Apr 08 11:39:45 2011 +0200
    27.2 +++ b/src/Pure/IsaMakefile	Fri Apr 08 13:31:16 2011 +0200
    27.3 @@ -185,9 +185,9 @@
    27.4    Syntax/printer.ML					\
    27.5    Syntax/simple_syntax.ML				\
    27.6    Syntax/syn_ext.ML					\
    27.7 -  Syntax/syn_trans.ML					\
    27.8    Syntax/syntax.ML					\
    27.9    Syntax/syntax_phases.ML				\
   27.10 +  Syntax/syntax_trans.ML				\
   27.11    Syntax/term_position.ML				\
   27.12    System/isabelle_process.ML				\
   27.13    System/isabelle_system.ML				\
    28.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 08 11:39:45 2011 +0200
    28.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 08 13:31:16 2011 +0200
    28.3 @@ -407,7 +407,7 @@
    28.4    register_config Syntax.show_structs_raw #>
    28.5    register_config Syntax.show_question_marks_raw #>
    28.6    register_config Syntax.ambiguity_level_raw #>
    28.7 -  register_config Syntax.eta_contract_raw #>
    28.8 +  register_config Syntax_Trans.eta_contract_raw #>
    28.9    register_config ML_Context.trace_raw #>
   28.10    register_config ProofContext.show_abbrevs_raw #>
   28.11    register_config Goal_Display.goals_limit_raw #>
    29.1 --- a/src/Pure/Isar/obtain.ML	Fri Apr 08 11:39:45 2011 +0200
    29.2 +++ b/src/Pure/Isar/obtain.ML	Fri Apr 08 13:31:16 2011 +0200
    29.3 @@ -231,7 +231,7 @@
    29.4        handle Type.TUNIFY =>
    29.5          err ("Failed to unify variable " ^
    29.6            string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
    29.7 -          string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
    29.8 +          string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
    29.9      val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
   29.10        (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
   29.11      val norm_type = Envir.norm_type tyenv;
    30.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 11:39:45 2011 +0200
    30.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 13:31:16 2011 +0200
    30.3 @@ -133,7 +133,7 @@
    30.4    bool_pref Goal_Display.show_main_goal_default
    30.5      "show-main-goal"
    30.6      "Show main goal in proof state display",
    30.7 -  bool_pref Syntax.eta_contract_default
    30.8 +  bool_pref Syntax_Trans.eta_contract_default
    30.9      "eta-contract"
   30.10      "Print terms eta-contracted"];
   30.11  
    31.1 --- a/src/Pure/ROOT.ML	Fri Apr 08 11:39:45 2011 +0200
    31.2 +++ b/src/Pure/ROOT.ML	Fri Apr 08 13:31:16 2011 +0200
    31.3 @@ -124,7 +124,7 @@
    31.4  use "Syntax/ast.ML";
    31.5  use "Syntax/syn_ext.ML";
    31.6  use "Syntax/parser.ML";
    31.7 -use "Syntax/syn_trans.ML";
    31.8 +use "Syntax/syntax_trans.ML";
    31.9  use "Syntax/mixfix.ML";
   31.10  use "Syntax/printer.ML";
   31.11  use "Syntax/syntax.ML";
    32.1 --- a/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 11:39:45 2011 +0200
    32.2 +++ b/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 13:31:16 2011 +0200
    32.3 @@ -58,7 +58,7 @@
    32.4        | update_gram ((false, add, m), decls) =
    32.5            Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    32.6  
    32.7 -    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    32.8 +    val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
    32.9      val local_syntax = thy_syntax
   32.10        |> Syntax.update_trfuns
   32.11            (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    33.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 11:39:45 2011 +0200
    33.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 13:31:16 2011 +0200
    33.3 @@ -154,10 +154,10 @@
    33.4      val xconsts = map #1 const_decls;
    33.5      val binders = map_filter binder const_decls;
    33.6      val binder_trs = binders
    33.7 -      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
    33.8 +      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
    33.9      val binder_trs' = binders
   33.10        |> map (Syn_Ext.stamp_trfun binder_stamp o
   33.11 -          apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
   33.12 +          apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   33.13    in
   33.14      Syn_Ext.syn_ext' true is_logtype
   33.15        mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    34.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 08 11:39:45 2011 +0200
    34.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 13:31:16 2011 +0200
    34.3 @@ -173,9 +173,9 @@
    34.4  
    34.5      (*default applications: prefix / postfix*)
    34.6      val appT =
    34.7 -      if type_mode then Syn_Trans.tappl_ast_tr'
    34.8 -      else if curried then Syn_Trans.applC_ast_tr'
    34.9 -      else Syn_Trans.appl_ast_tr';
   34.10 +      if type_mode then Syntax_Trans.tappl_ast_tr'
   34.11 +      else if curried then Syntax_Trans.applC_ast_tr'
   34.12 +      else Syntax_Trans.appl_ast_tr';
   34.13  
   34.14      fun synT _ ([], args) = ([], args)
   34.15        | synT m (Arg p :: symbs, t :: args) =
    35.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Apr 08 11:39:45 2011 +0200
    35.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.3 @@ -1,560 +0,0 @@
    35.4 -(*  Title:      Pure/Syntax/syn_trans.ML
    35.5 -    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    35.6 -
    35.7 -Syntax translation functions.
    35.8 -*)
    35.9 -
   35.10 -signature SYN_TRANS0 =
   35.11 -sig
   35.12 -  val eta_contract_default: bool Unsynchronized.ref
   35.13 -  val eta_contract_raw: Config.raw
   35.14 -  val eta_contract: bool Config.T
   35.15 -  val atomic_abs_tr': string * typ * term -> term * term
   35.16 -  val const_abs_tr': term -> term
   35.17 -  val mk_binder_tr: string * string -> string * (term list -> term)
   35.18 -  val mk_binder_tr': string * string -> string * (term list -> term)
   35.19 -  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   35.20 -  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
   35.21 -  val dependent_tr': string * string -> term list -> term
   35.22 -  val antiquote_tr: string -> term -> term
   35.23 -  val quote_tr: string -> term -> term
   35.24 -  val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
   35.25 -  val antiquote_tr': string -> term -> term
   35.26 -  val quote_tr': string -> term -> term
   35.27 -  val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
   35.28 -  val update_name_tr': term -> term
   35.29 -  val mark_bound: string -> term
   35.30 -  val mark_boundT: string * typ -> term
   35.31 -  val bound_vars: (string * typ) list -> term -> term
   35.32 -  val variant_abs: string * typ * term -> string * term
   35.33 -  val variant_abs': string * typ * term -> string * term
   35.34 -end;
   35.35 -
   35.36 -signature SYN_TRANS1 =
   35.37 -sig
   35.38 -  include SYN_TRANS0
   35.39 -  val no_brackets: unit -> bool
   35.40 -  val no_type_brackets: unit -> bool
   35.41 -  val non_typed_tr': (term list -> term) -> typ -> term list -> term
   35.42 -  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
   35.43 -  val constrainAbsC: string
   35.44 -  val abs_tr: term list -> term
   35.45 -  val pure_trfuns:
   35.46 -    (string * (Ast.ast list -> Ast.ast)) list *
   35.47 -    (string * (term list -> term)) list *
   35.48 -    (string * (term list -> term)) list *
   35.49 -    (string * (Ast.ast list -> Ast.ast)) list
   35.50 -  val struct_trfuns: string list ->
   35.51 -    (string * (Ast.ast list -> Ast.ast)) list *
   35.52 -    (string * (term list -> term)) list *
   35.53 -    (string * (typ -> term list -> term)) list *
   35.54 -    (string * (Ast.ast list -> Ast.ast)) list
   35.55 -end;
   35.56 -
   35.57 -signature SYN_TRANS =
   35.58 -sig
   35.59 -  include SYN_TRANS1
   35.60 -  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   35.61 -  val abs_tr': Proof.context -> term -> term
   35.62 -  val prop_tr': term -> term
   35.63 -  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   35.64 -  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   35.65 -end;
   35.66 -
   35.67 -structure Syn_Trans: SYN_TRANS =
   35.68 -struct
   35.69 -
   35.70 -(* print mode *)
   35.71 -
   35.72 -val bracketsN = "brackets";
   35.73 -val no_bracketsN = "no_brackets";
   35.74 -
   35.75 -fun no_brackets () =
   35.76 -  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
   35.77 -    (print_mode_value ()) = SOME no_bracketsN;
   35.78 -
   35.79 -val type_bracketsN = "type_brackets";
   35.80 -val no_type_bracketsN = "no_type_brackets";
   35.81 -
   35.82 -fun no_type_brackets () =
   35.83 -  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
   35.84 -    (print_mode_value ()) <> SOME type_bracketsN;
   35.85 -
   35.86 -
   35.87 -
   35.88 -(** parse (ast) translations **)
   35.89 -
   35.90 -(* strip_positions *)
   35.91 -
   35.92 -fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
   35.93 -  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
   35.94 -
   35.95 -
   35.96 -(* constify *)
   35.97 -
   35.98 -fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
   35.99 -  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
  35.100 -
  35.101 -
  35.102 -(* type syntax *)
  35.103 -
  35.104 -fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
  35.105 -  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
  35.106 -
  35.107 -fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
  35.108 -  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
  35.109 -
  35.110 -fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
  35.111 -  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
  35.112 -
  35.113 -
  35.114 -(* application *)
  35.115 -
  35.116 -fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
  35.117 -  | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
  35.118 -
  35.119 -fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
  35.120 -  | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
  35.121 -
  35.122 -
  35.123 -(* abstraction *)
  35.124 -
  35.125 -fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
  35.126 -  | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
  35.127 -
  35.128 -fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
  35.129 -  | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
  35.130 -
  35.131 -fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
  35.132 -  | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
  35.133 -
  35.134 -val constrainAbsC = "_constrainAbs";
  35.135 -
  35.136 -fun absfree_proper (x, T, t) =
  35.137 -  if can Name.dest_internal x
  35.138 -  then error ("Illegal internal variable in abstraction: " ^ quote x)
  35.139 -  else Term.absfree (x, T, t);
  35.140 -
  35.141 -fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
  35.142 -  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
  35.143 -  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT
  35.144 -  | abs_tr ts = raise TERM ("abs_tr", ts);
  35.145 -
  35.146 -
  35.147 -(* binder *)
  35.148 -
  35.149 -fun mk_binder_tr (syn, name) =
  35.150 -  let
  35.151 -    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
  35.152 -    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
  35.153 -      | binder_tr [x, t] =
  35.154 -          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
  35.155 -          in Lexicon.const name $ abs end
  35.156 -      | binder_tr ts = err ts;
  35.157 -  in (syn, binder_tr) end;
  35.158 -
  35.159 -
  35.160 -(* type propositions *)
  35.161 -
  35.162 -fun mk_type ty =
  35.163 -  Lexicon.const "_constrain" $
  35.164 -    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
  35.165 -
  35.166 -fun ofclass_tr [ty, cls] = cls $ mk_type ty
  35.167 -  | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
  35.168 -
  35.169 -fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
  35.170 -  | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
  35.171 -
  35.172 -
  35.173 -(* meta propositions *)
  35.174 -
  35.175 -fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
  35.176 -  | aprop_tr ts = raise TERM ("aprop_tr", ts);
  35.177 -
  35.178 -
  35.179 -(* meta implication *)
  35.180 -
  35.181 -fun bigimpl_ast_tr (asts as [asms, concl]) =
  35.182 -      let val prems =
  35.183 -        (case Ast.unfold_ast_p "_asms" asms of
  35.184 -          (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
  35.185 -        | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
  35.186 -      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
  35.187 -  | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
  35.188 -
  35.189 -
  35.190 -(* type/term reflection *)
  35.191 -
  35.192 -fun type_tr [ty] = mk_type ty
  35.193 -  | type_tr ts = raise TERM ("type_tr", ts);
  35.194 -
  35.195 -
  35.196 -(* dddot *)
  35.197 -
  35.198 -fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
  35.199 -
  35.200 -
  35.201 -(* quote / antiquote *)
  35.202 -
  35.203 -fun antiquote_tr name =
  35.204 -  let
  35.205 -    fun tr i ((t as Const (c, _)) $ u) =
  35.206 -          if c = name then tr i u $ Bound i
  35.207 -          else tr i t $ tr i u
  35.208 -      | tr i (t $ u) = tr i t $ tr i u
  35.209 -      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
  35.210 -      | tr _ a = a;
  35.211 -  in tr 0 end;
  35.212 -
  35.213 -fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
  35.214 -
  35.215 -fun quote_antiquote_tr quoteN antiquoteN name =
  35.216 -  let
  35.217 -    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
  35.218 -      | tr ts = raise TERM ("quote_tr", ts);
  35.219 -  in (quoteN, tr) end;
  35.220 -
  35.221 -
  35.222 -(* corresponding updates *)
  35.223 -
  35.224 -fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
  35.225 -  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
  35.226 -  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
  35.227 -      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
  35.228 -      else
  35.229 -        list_comb (c $ update_name_tr [t] $
  35.230 -          (Lexicon.fun_type $
  35.231 -            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
  35.232 -  | update_name_tr ts = raise TERM ("update_name_tr", ts);
  35.233 -
  35.234 -
  35.235 -(* indexed syntax *)
  35.236 -
  35.237 -fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
  35.238 -  | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
  35.239 -
  35.240 -fun index_ast_tr ast =
  35.241 -  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
  35.242 -
  35.243 -fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
  35.244 -  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
  35.245 -
  35.246 -fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
  35.247 -  | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
  35.248 -
  35.249 -fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
  35.250 -  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
  35.251 -
  35.252 -fun index_tr [t] = t
  35.253 -  | index_tr ts = raise TERM ("index_tr", ts);
  35.254 -
  35.255 -
  35.256 -(* implicit structures *)
  35.257 -
  35.258 -fun the_struct structs i =
  35.259 -  if 1 <= i andalso i <= length structs then nth structs (i - 1)
  35.260 -  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
  35.261 -
  35.262 -fun struct_tr structs [Const ("_indexdefault", _)] =
  35.263 -      Lexicon.free (the_struct structs 1)
  35.264 -  | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
  35.265 -      Lexicon.free (the_struct structs
  35.266 -        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
  35.267 -  | struct_tr _ ts = raise TERM ("struct_tr", ts);
  35.268 -
  35.269 -
  35.270 -
  35.271 -(** print (ast) translations **)
  35.272 -
  35.273 -(* types *)
  35.274 -
  35.275 -fun non_typed_tr' f _ ts = f ts;
  35.276 -fun non_typed_tr'' f x _ ts = f x ts;
  35.277 -
  35.278 -
  35.279 -(* type syntax *)
  35.280 -
  35.281 -fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
  35.282 -  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
  35.283 -  | tappl_ast_tr' (f, ty :: tys) =
  35.284 -      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
  35.285 -
  35.286 -fun fun_ast_tr' asts =
  35.287 -  if no_brackets () orelse no_type_brackets () then raise Match
  35.288 -  else
  35.289 -    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
  35.290 -      (dom as _ :: _ :: _, cod)
  35.291 -        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
  35.292 -    | _ => raise Match);
  35.293 -
  35.294 -
  35.295 -(* application *)
  35.296 -
  35.297 -fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
  35.298 -  | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
  35.299 -
  35.300 -fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
  35.301 -  | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
  35.302 -
  35.303 -
  35.304 -(* partial eta-contraction before printing *)
  35.305 -
  35.306 -fun eta_abs (Abs (a, T, t)) =
  35.307 -      (case eta_abs t of
  35.308 -        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
  35.309 -      | t' as f $ u =>
  35.310 -          (case eta_abs u of
  35.311 -            Bound 0 =>
  35.312 -              if Term.is_dependent f then Abs (a, T, t')
  35.313 -              else incr_boundvars ~1 f
  35.314 -          | _ => Abs (a, T, t'))
  35.315 -      | t' => Abs (a, T, t'))
  35.316 -  | eta_abs t = t;
  35.317 -
  35.318 -val eta_contract_default = Unsynchronized.ref true;
  35.319 -val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
  35.320 -val eta_contract = Config.bool eta_contract_raw;
  35.321 -
  35.322 -fun eta_contr ctxt tm =
  35.323 -  if Config.get ctxt eta_contract then eta_abs tm else tm;
  35.324 -
  35.325 -
  35.326 -(* abstraction *)
  35.327 -
  35.328 -fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
  35.329 -fun mark_bound x = mark_boundT (x, dummyT);
  35.330 -
  35.331 -fun bound_vars vars body =
  35.332 -  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
  35.333 -
  35.334 -fun strip_abss vars_of body_of tm =
  35.335 -  let
  35.336 -    val vars = vars_of tm;
  35.337 -    val body = body_of tm;
  35.338 -    val rev_new_vars = Term.rename_wrt_term body vars;
  35.339 -    fun subst (x, T) b =
  35.340 -      if can Name.dest_internal x andalso not (Term.is_dependent b)
  35.341 -      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
  35.342 -      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
  35.343 -    val (rev_vars', body') = fold_map subst rev_new_vars body;
  35.344 -  in (rev rev_vars', body') end;
  35.345 -
  35.346 -
  35.347 -fun abs_tr' ctxt tm =
  35.348 -  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
  35.349 -    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
  35.350 -
  35.351 -fun atomic_abs_tr' (x, T, t) =
  35.352 -  let val [xT] = Term.rename_wrt_term t [(x, T)]
  35.353 -  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
  35.354 -
  35.355 -fun abs_ast_tr' asts =
  35.356 -  (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
  35.357 -    ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
  35.358 -  | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
  35.359 -
  35.360 -fun const_abs_tr' t =
  35.361 -  (case eta_abs t of
  35.362 -    Abs (_, _, t') =>
  35.363 -      if Term.is_dependent t' then raise Match
  35.364 -      else incr_boundvars ~1 t'
  35.365 -  | _ => raise Match);
  35.366 -
  35.367 -
  35.368 -(* binders *)
  35.369 -
  35.370 -fun mk_binder_tr' (name, syn) =
  35.371 -  let
  35.372 -    fun mk_idts [] = raise Match    (*abort translation*)
  35.373 -      | mk_idts [idt] = idt
  35.374 -      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
  35.375 -
  35.376 -    fun tr' t =
  35.377 -      let
  35.378 -        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
  35.379 -      in Lexicon.const syn $ mk_idts xs $ bd end;
  35.380 -
  35.381 -    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
  35.382 -      | binder_tr' [] = raise Match;
  35.383 -  in (name, binder_tr') end;
  35.384 -
  35.385 -fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
  35.386 -  let val (x, t) = atomic_abs_tr' abs
  35.387 -  in list_comb (Lexicon.const syn $ x $ t, ts) end);
  35.388 -
  35.389 -fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
  35.390 -  let val (x, t) = atomic_abs_tr' abs
  35.391 -  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
  35.392 -
  35.393 -
  35.394 -(* idtyp constraints *)
  35.395 -
  35.396 -fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
  35.397 -      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
  35.398 -  | idtyp_ast_tr' _ _ = raise Match;
  35.399 -
  35.400 -
  35.401 -(* meta propositions *)
  35.402 -
  35.403 -fun prop_tr' tm =
  35.404 -  let
  35.405 -    fun aprop t = Lexicon.const "_aprop" $ t;
  35.406 -
  35.407 -    fun is_prop Ts t =
  35.408 -      fastype_of1 (Ts, t) = propT handle TERM _ => false;
  35.409 -
  35.410 -    fun is_term (Const ("Pure.term", _) $ _) = true
  35.411 -      | is_term _ = false;
  35.412 -
  35.413 -    fun tr' _ (t as Const _) = t
  35.414 -      | tr' Ts (t as Const ("_bound", _) $ u) =
  35.415 -          if is_prop Ts u then aprop t else t
  35.416 -      | tr' _ (t as Free (x, T)) =
  35.417 -          if T = propT then aprop (Lexicon.free x) else t
  35.418 -      | tr' _ (t as Var (xi, T)) =
  35.419 -          if T = propT then aprop (Lexicon.var xi) else t
  35.420 -      | tr' Ts (t as Bound _) =
  35.421 -          if is_prop Ts t then aprop t else t
  35.422 -      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
  35.423 -      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
  35.424 -          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
  35.425 -          else tr' Ts t1 $ tr' Ts t2
  35.426 -      | tr' Ts (t as t1 $ t2) =
  35.427 -          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
  35.428 -            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
  35.429 -  in tr' [] tm end;
  35.430 -
  35.431 -
  35.432 -(* meta implication *)
  35.433 -
  35.434 -fun impl_ast_tr' asts =
  35.435 -  if no_brackets () then raise Match
  35.436 -  else
  35.437 -    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
  35.438 -      (prems as _ :: _ :: _, concl) =>
  35.439 -        let
  35.440 -          val (asms, asm) = split_last prems;
  35.441 -          val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
  35.442 -        in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
  35.443 -    | _ => raise Match);
  35.444 -
  35.445 -
  35.446 -(* dependent / nondependent quantifiers *)
  35.447 -
  35.448 -fun var_abs mark (x, T, b) =
  35.449 -  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
  35.450 -  in (x', subst_bound (mark (x', T), b)) end;
  35.451 -
  35.452 -val variant_abs = var_abs Free;
  35.453 -val variant_abs' = var_abs mark_boundT;
  35.454 -
  35.455 -fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
  35.456 -      if Term.is_dependent B then
  35.457 -        let val (x', B') = variant_abs' (x, dummyT, B);
  35.458 -        in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
  35.459 -      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
  35.460 -  | dependent_tr' _ _ = raise Match;
  35.461 -
  35.462 -
  35.463 -(* quote / antiquote *)
  35.464 -
  35.465 -fun antiquote_tr' name =
  35.466 -  let
  35.467 -    fun tr' i (t $ u) =
  35.468 -          if u aconv Bound i then Lexicon.const name $ tr' i t
  35.469 -          else tr' i t $ tr' i u
  35.470 -      | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
  35.471 -      | tr' i a = if a aconv Bound i then raise Match else a;
  35.472 -  in tr' 0 end;
  35.473 -
  35.474 -fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
  35.475 -  | quote_tr' _ _ = raise Match;
  35.476 -
  35.477 -fun quote_antiquote_tr' quoteN antiquoteN name =
  35.478 -  let
  35.479 -    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
  35.480 -      | tr' _ = raise Match;
  35.481 -  in (name, tr') end;
  35.482 -
  35.483 -
  35.484 -(* corresponding updates *)
  35.485 -
  35.486 -local
  35.487 -
  35.488 -fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
  35.489 -  | upd_type _ = dummyT;
  35.490 -
  35.491 -fun upd_tr' (x_upd, T) =
  35.492 -  (case try (unsuffix "_update") x_upd of
  35.493 -    SOME x => (x, upd_type T)
  35.494 -  | NONE => raise Match);
  35.495 -
  35.496 -in
  35.497 -
  35.498 -fun update_name_tr' (Free x) = Free (upd_tr' x)
  35.499 -  | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
  35.500 -  | update_name_tr' (Const x) = Const (upd_tr' x)
  35.501 -  | update_name_tr' _ = raise Match;
  35.502 -
  35.503 -end;
  35.504 -
  35.505 -
  35.506 -(* indexed syntax *)
  35.507 -
  35.508 -fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
  35.509 -  | index_ast_tr' _ = raise Match;
  35.510 -
  35.511 -
  35.512 -(* implicit structures *)
  35.513 -
  35.514 -fun the_struct' structs s =
  35.515 -  [(case Lexicon.read_nat s of
  35.516 -    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
  35.517 -  | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
  35.518 -
  35.519 -fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
  35.520 -  | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
  35.521 -      the_struct' structs s
  35.522 -  | struct_ast_tr' _ _ = raise Match;
  35.523 -
  35.524 -
  35.525 -
  35.526 -(** Pure translations **)
  35.527 -
  35.528 -val pure_trfuns =
  35.529 -  ([("_strip_positions", strip_positions_ast_tr),
  35.530 -    ("_constify", constify_ast_tr),
  35.531 -    ("_tapp", tapp_ast_tr),
  35.532 -    ("_tappl", tappl_ast_tr),
  35.533 -    ("_bracket", bracket_ast_tr),
  35.534 -    ("_appl", appl_ast_tr),
  35.535 -    ("_applC", applC_ast_tr),
  35.536 -    ("_lambda", lambda_ast_tr),
  35.537 -    ("_idtyp", idtyp_ast_tr),
  35.538 -    ("_idtypdummy", idtypdummy_ast_tr),
  35.539 -    ("_bigimpl", bigimpl_ast_tr),
  35.540 -    ("_indexdefault", indexdefault_ast_tr),
  35.541 -    ("_indexnum", indexnum_ast_tr),
  35.542 -    ("_indexvar", indexvar_ast_tr),
  35.543 -    ("_struct", struct_ast_tr)],
  35.544 -   [("_abs", abs_tr),
  35.545 -    ("_aprop", aprop_tr),
  35.546 -    ("_ofclass", ofclass_tr),
  35.547 -    ("_sort_constraint", sort_constraint_tr),
  35.548 -    ("_TYPE", type_tr),
  35.549 -    ("_DDDOT", dddot_tr),
  35.550 -    ("_update_name", update_name_tr),
  35.551 -    ("_index", index_tr)],
  35.552 -   ([]: (string * (term list -> term)) list),
  35.553 -   [("\\<^type>fun", fun_ast_tr'),
  35.554 -    ("_abs", abs_ast_tr'),
  35.555 -    ("_idts", idtyp_ast_tr' "_idts"),
  35.556 -    ("_pttrns", idtyp_ast_tr' "_pttrns"),
  35.557 -    ("\\<^const>==>", impl_ast_tr'),
  35.558 -    ("_index", index_ast_tr')]);
  35.559 -
  35.560 -fun struct_trfuns structs =
  35.561 -  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
  35.562 -
  35.563 -end;
    36.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 11:39:45 2011 +0200
    36.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 13:31:16 2011 +0200
    36.3 @@ -7,7 +7,6 @@
    36.4  
    36.5  signature BASIC_SYNTAX =
    36.6  sig
    36.7 -  include SYN_TRANS0
    36.8    include MIXFIX0
    36.9    include PRINTER0
   36.10  end;
   36.11 @@ -16,7 +15,6 @@
   36.12  sig
   36.13    include LEXICON0
   36.14    include SYN_EXT0
   36.15 -  include SYN_TRANS1
   36.16    include MIXFIX1
   36.17    include PRINTER0
   36.18    val positions_raw: Config.raw
   36.19 @@ -727,7 +725,7 @@
   36.20  
   36.21  (*export parts of internal Syntax structures*)
   36.22  val syntax_tokenize = tokenize;
   36.23 -open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
   36.24 +open Lexicon Syn_Ext Mixfix Printer;
   36.25  val tokenize = syntax_tokenize;
   36.26  
   36.27  end;
    37.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 11:39:45 2011 +0200
    37.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 13:31:16 2011 +0200
    37.3 @@ -532,7 +532,7 @@
    37.4  
    37.5      fun ast_of tm =
    37.6        (case strip_comb tm of
    37.7 -        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
    37.8 +        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
    37.9        | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   37.10            Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   37.11        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   37.12 @@ -557,7 +557,7 @@
   37.13        else simple_ast_of ctxt t;
   37.14    in
   37.15      tm
   37.16 -    |> Syn_Trans.prop_tr'
   37.17 +    |> Syntax_Trans.prop_tr'
   37.18      |> show_types ? (#1 o prune_typs o rpair [])
   37.19      |> mark_atoms
   37.20      |> ast_of
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Fri Apr 08 13:31:16 2011 +0200
    38.3 @@ -0,0 +1,556 @@
    38.4 +(*  Title:      Pure/Syntax/syntax_trans.ML
    38.5 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    38.6 +
    38.7 +Syntax translation functions.
    38.8 +*)
    38.9 +
   38.10 +signature BASIC_SYNTAX_TRANS =
   38.11 +sig
   38.12 +  val eta_contract: bool Config.T
   38.13 +end
   38.14 +
   38.15 +signature SYNTAX_TRANS =
   38.16 +sig
   38.17 +  include BASIC_SYNTAX_TRANS
   38.18 +  val no_brackets: unit -> bool
   38.19 +  val no_type_brackets: unit -> bool
   38.20 +  val abs_tr: term list -> term
   38.21 +  val mk_binder_tr: string * string -> string * (term list -> term)
   38.22 +  val antiquote_tr: string -> term -> term
   38.23 +  val quote_tr: string -> term -> term
   38.24 +  val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
   38.25 +  val non_typed_tr': (term list -> term) -> typ -> term list -> term
   38.26 +  val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
   38.27 +  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   38.28 +  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   38.29 +  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   38.30 +  val eta_contract_default: bool Unsynchronized.ref
   38.31 +  val eta_contract_raw: Config.raw
   38.32 +  val mark_bound: string -> term
   38.33 +  val mark_boundT: string * typ -> term
   38.34 +  val bound_vars: (string * typ) list -> term -> term
   38.35 +  val abs_tr': Proof.context -> term -> term
   38.36 +  val atomic_abs_tr': string * typ * term -> term * term
   38.37 +  val const_abs_tr': term -> term
   38.38 +  val mk_binder_tr': string * string -> string * (term list -> term)
   38.39 +  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
   38.40 +  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
   38.41 +  val prop_tr': term -> term
   38.42 +  val variant_abs: string * typ * term -> string * term
   38.43 +  val variant_abs': string * typ * term -> string * term
   38.44 +  val dependent_tr': string * string -> term list -> term
   38.45 +  val antiquote_tr': string -> term -> term
   38.46 +  val quote_tr': string -> term -> term
   38.47 +  val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
   38.48 +  val update_name_tr': term -> term
   38.49 +  val pure_trfuns:
   38.50 +    (string * (Ast.ast list -> Ast.ast)) list *
   38.51 +    (string * (term list -> term)) list *
   38.52 +    (string * (term list -> term)) list *
   38.53 +    (string * (Ast.ast list -> Ast.ast)) list
   38.54 +  val struct_trfuns: string list ->
   38.55 +    (string * (Ast.ast list -> Ast.ast)) list *
   38.56 +    (string * (term list -> term)) list *
   38.57 +    (string * (typ -> term list -> term)) list *
   38.58 +    (string * (Ast.ast list -> Ast.ast)) list
   38.59 +end;
   38.60 +
   38.61 +structure Syntax_Trans: SYNTAX_TRANS =
   38.62 +struct
   38.63 +
   38.64 +(* print mode *)
   38.65 +
   38.66 +val bracketsN = "brackets";
   38.67 +val no_bracketsN = "no_brackets";
   38.68 +
   38.69 +fun no_brackets () =
   38.70 +  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
   38.71 +    (print_mode_value ()) = SOME no_bracketsN;
   38.72 +
   38.73 +val type_bracketsN = "type_brackets";
   38.74 +val no_type_bracketsN = "no_type_brackets";
   38.75 +
   38.76 +fun no_type_brackets () =
   38.77 +  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
   38.78 +    (print_mode_value ()) <> SOME type_bracketsN;
   38.79 +
   38.80 +
   38.81 +
   38.82 +(** parse (ast) translations **)
   38.83 +
   38.84 +(* strip_positions *)
   38.85 +
   38.86 +fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
   38.87 +  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
   38.88 +
   38.89 +
   38.90 +(* constify *)
   38.91 +
   38.92 +fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
   38.93 +  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
   38.94 +
   38.95 +
   38.96 +(* type syntax *)
   38.97 +
   38.98 +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
   38.99 +  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
  38.100 +
  38.101 +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
  38.102 +  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
  38.103 +
  38.104 +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
  38.105 +  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
  38.106 +
  38.107 +
  38.108 +(* application *)
  38.109 +
  38.110 +fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
  38.111 +  | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
  38.112 +
  38.113 +fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
  38.114 +  | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
  38.115 +
  38.116 +
  38.117 +(* abstraction *)
  38.118 +
  38.119 +fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
  38.120 +  | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
  38.121 +
  38.122 +fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
  38.123 +  | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
  38.124 +
  38.125 +fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
  38.126 +  | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
  38.127 +
  38.128 +fun absfree_proper (x, T, t) =
  38.129 +  if can Name.dest_internal x
  38.130 +  then error ("Illegal internal variable in abstraction: " ^ quote x)
  38.131 +  else Term.absfree (x, T, t);
  38.132 +
  38.133 +fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
  38.134 +  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
  38.135 +  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
  38.136 +      Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT
  38.137 +  | abs_tr ts = raise TERM ("abs_tr", ts);
  38.138 +
  38.139 +
  38.140 +(* binder *)
  38.141 +
  38.142 +fun mk_binder_tr (syn, name) =
  38.143 +  let
  38.144 +    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
  38.145 +    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
  38.146 +      | binder_tr [x, t] =
  38.147 +          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
  38.148 +          in Lexicon.const name $ abs end
  38.149 +      | binder_tr ts = err ts;
  38.150 +  in (syn, binder_tr) end;
  38.151 +
  38.152 +
  38.153 +(* type propositions *)
  38.154 +
  38.155 +fun mk_type ty =
  38.156 +  Lexicon.const "_constrain" $
  38.157 +    Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
  38.158 +
  38.159 +fun ofclass_tr [ty, cls] = cls $ mk_type ty
  38.160 +  | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
  38.161 +
  38.162 +fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
  38.163 +  | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
  38.164 +
  38.165 +
  38.166 +(* meta propositions *)
  38.167 +
  38.168 +fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
  38.169 +  | aprop_tr ts = raise TERM ("aprop_tr", ts);
  38.170 +
  38.171 +
  38.172 +(* meta implication *)
  38.173 +
  38.174 +fun bigimpl_ast_tr (asts as [asms, concl]) =
  38.175 +      let val prems =
  38.176 +        (case Ast.unfold_ast_p "_asms" asms of
  38.177 +          (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
  38.178 +        | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
  38.179 +      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
  38.180 +  | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
  38.181 +
  38.182 +
  38.183 +(* type/term reflection *)
  38.184 +
  38.185 +fun type_tr [ty] = mk_type ty
  38.186 +  | type_tr ts = raise TERM ("type_tr", ts);
  38.187 +
  38.188 +
  38.189 +(* dddot *)
  38.190 +
  38.191 +fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
  38.192 +
  38.193 +
  38.194 +(* quote / antiquote *)
  38.195 +
  38.196 +fun antiquote_tr name =
  38.197 +  let
  38.198 +    fun tr i ((t as Const (c, _)) $ u) =
  38.199 +          if c = name then tr i u $ Bound i
  38.200 +          else tr i t $ tr i u
  38.201 +      | tr i (t $ u) = tr i t $ tr i u
  38.202 +      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
  38.203 +      | tr _ a = a;
  38.204 +  in tr 0 end;
  38.205 +
  38.206 +fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
  38.207 +
  38.208 +fun quote_antiquote_tr quoteN antiquoteN name =
  38.209 +  let
  38.210 +    fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
  38.211 +      | tr ts = raise TERM ("quote_tr", ts);
  38.212 +  in (quoteN, tr) end;
  38.213 +
  38.214 +
  38.215 +(* corresponding updates *)
  38.216 +
  38.217 +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
  38.218 +  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
  38.219 +  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
  38.220 +      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
  38.221 +      else
  38.222 +        list_comb (c $ update_name_tr [t] $
  38.223 +          (Lexicon.fun_type $
  38.224 +            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
  38.225 +  | update_name_tr ts = raise TERM ("update_name_tr", ts);
  38.226 +
  38.227 +
  38.228 +(* indexed syntax *)
  38.229 +
  38.230 +fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
  38.231 +  | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
  38.232 +
  38.233 +fun index_ast_tr ast =
  38.234 +  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
  38.235 +
  38.236 +fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
  38.237 +  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
  38.238 +
  38.239 +fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
  38.240 +  | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
  38.241 +
  38.242 +fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
  38.243 +  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
  38.244 +
  38.245 +fun index_tr [t] = t
  38.246 +  | index_tr ts = raise TERM ("index_tr", ts);
  38.247 +
  38.248 +
  38.249 +(* implicit structures *)
  38.250 +
  38.251 +fun the_struct structs i =
  38.252 +  if 1 <= i andalso i <= length structs then nth structs (i - 1)
  38.253 +  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
  38.254 +
  38.255 +fun struct_tr structs [Const ("_indexdefault", _)] =
  38.256 +      Lexicon.free (the_struct structs 1)
  38.257 +  | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
  38.258 +      Lexicon.free (the_struct structs
  38.259 +        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
  38.260 +  | struct_tr _ ts = raise TERM ("struct_tr", ts);
  38.261 +
  38.262 +
  38.263 +
  38.264 +(** print (ast) translations **)
  38.265 +
  38.266 +(* types *)
  38.267 +
  38.268 +fun non_typed_tr' f _ ts = f ts;
  38.269 +fun non_typed_tr'' f x _ ts = f x ts;
  38.270 +
  38.271 +
  38.272 +(* type syntax *)
  38.273 +
  38.274 +fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
  38.275 +  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
  38.276 +  | tappl_ast_tr' (f, ty :: tys) =
  38.277 +      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
  38.278 +
  38.279 +fun fun_ast_tr' asts =
  38.280 +  if no_brackets () orelse no_type_brackets () then raise Match
  38.281 +  else
  38.282 +    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
  38.283 +      (dom as _ :: _ :: _, cod)
  38.284 +        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
  38.285 +    | _ => raise Match);
  38.286 +
  38.287 +
  38.288 +(* application *)
  38.289 +
  38.290 +fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
  38.291 +  | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
  38.292 +
  38.293 +fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
  38.294 +  | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
  38.295 +
  38.296 +
  38.297 +(* partial eta-contraction before printing *)
  38.298 +
  38.299 +fun eta_abs (Abs (a, T, t)) =
  38.300 +      (case eta_abs t of
  38.301 +        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
  38.302 +      | t' as f $ u =>
  38.303 +          (case eta_abs u of
  38.304 +            Bound 0 =>
  38.305 +              if Term.is_dependent f then Abs (a, T, t')
  38.306 +              else incr_boundvars ~1 f
  38.307 +          | _ => Abs (a, T, t'))
  38.308 +      | t' => Abs (a, T, t'))
  38.309 +  | eta_abs t = t;
  38.310 +
  38.311 +val eta_contract_default = Unsynchronized.ref true;
  38.312 +val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
  38.313 +val eta_contract = Config.bool eta_contract_raw;
  38.314 +
  38.315 +fun eta_contr ctxt tm =
  38.316 +  if Config.get ctxt eta_contract then eta_abs tm else tm;
  38.317 +
  38.318 +
  38.319 +(* abstraction *)
  38.320 +
  38.321 +fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
  38.322 +fun mark_bound x = mark_boundT (x, dummyT);
  38.323 +
  38.324 +fun bound_vars vars body =
  38.325 +  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
  38.326 +
  38.327 +fun strip_abss vars_of body_of tm =
  38.328 +  let
  38.329 +    val vars = vars_of tm;
  38.330 +    val body = body_of tm;
  38.331 +    val rev_new_vars = Term.rename_wrt_term body vars;
  38.332 +    fun subst (x, T) b =
  38.333 +      if can Name.dest_internal x andalso not (Term.is_dependent b)
  38.334 +      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
  38.335 +      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
  38.336 +    val (rev_vars', body') = fold_map subst rev_new_vars body;
  38.337 +  in (rev rev_vars', body') end;
  38.338 +
  38.339 +
  38.340 +fun abs_tr' ctxt tm =
  38.341 +  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
  38.342 +    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
  38.343 +
  38.344 +fun atomic_abs_tr' (x, T, t) =
  38.345 +  let val [xT] = Term.rename_wrt_term t [(x, T)]
  38.346 +  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
  38.347 +
  38.348 +fun abs_ast_tr' asts =
  38.349 +  (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
  38.350 +    ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
  38.351 +  | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
  38.352 +
  38.353 +fun const_abs_tr' t =
  38.354 +  (case eta_abs t of
  38.355 +    Abs (_, _, t') =>
  38.356 +      if Term.is_dependent t' then raise Match
  38.357 +      else incr_boundvars ~1 t'
  38.358 +  | _ => raise Match);
  38.359 +
  38.360 +
  38.361 +(* binders *)
  38.362 +
  38.363 +fun mk_binder_tr' (name, syn) =
  38.364 +  let
  38.365 +    fun mk_idts [] = raise Match    (*abort translation*)
  38.366 +      | mk_idts [idt] = idt
  38.367 +      | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
  38.368 +
  38.369 +    fun tr' t =
  38.370 +      let
  38.371 +        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
  38.372 +      in Lexicon.const syn $ mk_idts xs $ bd end;
  38.373 +
  38.374 +    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
  38.375 +      | binder_tr' [] = raise Match;
  38.376 +  in (name, binder_tr') end;
  38.377 +
  38.378 +fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
  38.379 +  let val (x, t) = atomic_abs_tr' abs
  38.380 +  in list_comb (Lexicon.const syn $ x $ t, ts) end);
  38.381 +
  38.382 +fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
  38.383 +  let val (x, t) = atomic_abs_tr' abs
  38.384 +  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
  38.385 +
  38.386 +
  38.387 +(* idtyp constraints *)
  38.388 +
  38.389 +fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
  38.390 +      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
  38.391 +  | idtyp_ast_tr' _ _ = raise Match;
  38.392 +
  38.393 +
  38.394 +(* meta propositions *)
  38.395 +
  38.396 +fun prop_tr' tm =
  38.397 +  let
  38.398 +    fun aprop t = Lexicon.const "_aprop" $ t;
  38.399 +
  38.400 +    fun is_prop Ts t =
  38.401 +      fastype_of1 (Ts, t) = propT handle TERM _ => false;
  38.402 +
  38.403 +    fun is_term (Const ("Pure.term", _) $ _) = true
  38.404 +      | is_term _ = false;
  38.405 +
  38.406 +    fun tr' _ (t as Const _) = t
  38.407 +      | tr' Ts (t as Const ("_bound", _) $ u) =
  38.408 +          if is_prop Ts u then aprop t else t
  38.409 +      | tr' _ (t as Free (x, T)) =
  38.410 +          if T = propT then aprop (Lexicon.free x) else t
  38.411 +      | tr' _ (t as Var (xi, T)) =
  38.412 +          if T = propT then aprop (Lexicon.var xi) else t
  38.413 +      | tr' Ts (t as Bound _) =
  38.414 +          if is_prop Ts t then aprop t else t
  38.415 +      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
  38.416 +      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
  38.417 +          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
  38.418 +          else tr' Ts t1 $ tr' Ts t2
  38.419 +      | tr' Ts (t as t1 $ t2) =
  38.420 +          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
  38.421 +            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
  38.422 +  in tr' [] tm end;
  38.423 +
  38.424 +
  38.425 +(* meta implication *)
  38.426 +
  38.427 +fun impl_ast_tr' asts =
  38.428 +  if no_brackets () then raise Match
  38.429 +  else
  38.430 +    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
  38.431 +      (prems as _ :: _ :: _, concl) =>
  38.432 +        let
  38.433 +          val (asms, asm) = split_last prems;
  38.434 +          val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
  38.435 +        in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
  38.436 +    | _ => raise Match);
  38.437 +
  38.438 +
  38.439 +(* dependent / nondependent quantifiers *)
  38.440 +
  38.441 +fun var_abs mark (x, T, b) =
  38.442 +  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
  38.443 +  in (x', subst_bound (mark (x', T), b)) end;
  38.444 +
  38.445 +val variant_abs = var_abs Free;
  38.446 +val variant_abs' = var_abs mark_boundT;
  38.447 +
  38.448 +fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
  38.449 +      if Term.is_dependent B then
  38.450 +        let val (x', B') = variant_abs' (x, dummyT, B);
  38.451 +        in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
  38.452 +      else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
  38.453 +  | dependent_tr' _ _ = raise Match;
  38.454 +
  38.455 +
  38.456 +(* quote / antiquote *)
  38.457 +
  38.458 +fun antiquote_tr' name =
  38.459 +  let
  38.460 +    fun tr' i (t $ u) =
  38.461 +          if u aconv Bound i then Lexicon.const name $ tr' i t
  38.462 +          else tr' i t $ tr' i u
  38.463 +      | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
  38.464 +      | tr' i a = if a aconv Bound i then raise Match else a;
  38.465 +  in tr' 0 end;
  38.466 +
  38.467 +fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
  38.468 +  | quote_tr' _ _ = raise Match;
  38.469 +
  38.470 +fun quote_antiquote_tr' quoteN antiquoteN name =
  38.471 +  let
  38.472 +    fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
  38.473 +      | tr' _ = raise Match;
  38.474 +  in (name, tr') end;
  38.475 +
  38.476 +
  38.477 +(* corresponding updates *)
  38.478 +
  38.479 +local
  38.480 +
  38.481 +fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
  38.482 +  | upd_type _ = dummyT;
  38.483 +
  38.484 +fun upd_tr' (x_upd, T) =
  38.485 +  (case try (unsuffix "_update") x_upd of
  38.486 +    SOME x => (x, upd_type T)
  38.487 +  | NONE => raise Match);
  38.488 +
  38.489 +in
  38.490 +
  38.491 +fun update_name_tr' (Free x) = Free (upd_tr' x)
  38.492 +  | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
  38.493 +  | update_name_tr' (Const x) = Const (upd_tr' x)
  38.494 +  | update_name_tr' _ = raise Match;
  38.495 +
  38.496 +end;
  38.497 +
  38.498 +
  38.499 +(* indexed syntax *)
  38.500 +
  38.501 +fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
  38.502 +  | index_ast_tr' _ = raise Match;
  38.503 +
  38.504 +
  38.505 +(* implicit structures *)
  38.506 +
  38.507 +fun the_struct' structs s =
  38.508 +  [(case Lexicon.read_nat s of
  38.509 +    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
  38.510 +  | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
  38.511 +
  38.512 +fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
  38.513 +  | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
  38.514 +      the_struct' structs s
  38.515 +  | struct_ast_tr' _ _ = raise Match;
  38.516 +
  38.517 +
  38.518 +
  38.519 +(** Pure translations **)
  38.520 +
  38.521 +val pure_trfuns =
  38.522 +  ([("_strip_positions", strip_positions_ast_tr),
  38.523 +    ("_constify", constify_ast_tr),
  38.524 +    ("_tapp", tapp_ast_tr),
  38.525 +    ("_tappl", tappl_ast_tr),
  38.526 +    ("_bracket", bracket_ast_tr),
  38.527 +    ("_appl", appl_ast_tr),
  38.528 +    ("_applC", applC_ast_tr),
  38.529 +    ("_lambda", lambda_ast_tr),
  38.530 +    ("_idtyp", idtyp_ast_tr),
  38.531 +    ("_idtypdummy", idtypdummy_ast_tr),
  38.532 +    ("_bigimpl", bigimpl_ast_tr),
  38.533 +    ("_indexdefault", indexdefault_ast_tr),
  38.534 +    ("_indexnum", indexnum_ast_tr),
  38.535 +    ("_indexvar", indexvar_ast_tr),
  38.536 +    ("_struct", struct_ast_tr)],
  38.537 +   [("_abs", abs_tr),
  38.538 +    ("_aprop", aprop_tr),
  38.539 +    ("_ofclass", ofclass_tr),
  38.540 +    ("_sort_constraint", sort_constraint_tr),
  38.541 +    ("_TYPE", type_tr),
  38.542 +    ("_DDDOT", dddot_tr),
  38.543 +    ("_update_name", update_name_tr),
  38.544 +    ("_index", index_tr)],
  38.545 +   ([]: (string * (term list -> term)) list),
  38.546 +   [("\\<^type>fun", fun_ast_tr'),
  38.547 +    ("_abs", abs_ast_tr'),
  38.548 +    ("_idts", idtyp_ast_tr' "_idts"),
  38.549 +    ("_pttrns", idtyp_ast_tr' "_pttrns"),
  38.550 +    ("\\<^const>==>", impl_ast_tr'),
  38.551 +    ("_index", index_ast_tr')]);
  38.552 +
  38.553 +fun struct_trfuns structs =
  38.554 +  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
  38.555 +
  38.556 +end;
  38.557 +
  38.558 +structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
  38.559 +open Basic_Syntax_Trans;
    39.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 08 11:39:45 2011 +0200
    39.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Apr 08 13:31:16 2011 +0200
    39.3 @@ -453,7 +453,7 @@
    39.4  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
    39.5  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
    39.6  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
    39.7 -val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
    39.8 +val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
    39.9  val _ = add_option "display" (Config.put display o boolean);
   39.10  val _ = add_option "break" (Config.put break o boolean);
   39.11  val _ = add_option "quotes" (Config.put quotes o boolean);
    40.1 --- a/src/Pure/primitive_defs.ML	Fri Apr 08 11:39:45 2011 +0200
    40.2 +++ b/src/Pure/primitive_defs.ML	Fri Apr 08 13:31:16 2011 +0200
    40.3 @@ -27,7 +27,7 @@
    40.4      val eq_body = Term.strip_all_body eq;
    40.5  
    40.6      val display_terms =
    40.7 -      commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
    40.8 +      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
    40.9      val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
   40.10  
   40.11      val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
    41.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 11:39:45 2011 +0200
    41.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 13:31:16 2011 +0200
    41.3 @@ -128,7 +128,7 @@
    41.4      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
    41.5      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
    41.6      ("_update_name", typ "idt",                        NoSyn),
    41.7 -    (Syntax.constrainAbsC, typ "'a",                   NoSyn),
    41.8 +    ("_constrainAbs", typ "'a",                       NoSyn),
    41.9      ("_constrain_position", typ "id => id_position",   Delimfix "_"),
   41.10      ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
   41.11      ("_type_constraint_", typ "'a",                    NoSyn),
   41.12 @@ -169,7 +169,7 @@
   41.13    #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
   41.14    #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
   41.15    #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   41.16 -  #> Sign.add_trfuns Syntax.pure_trfuns
   41.17 +  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
   41.18    #> Sign.local_path
   41.19    #> Sign.add_consts_i
   41.20     [(Binding.name "term", typ "'a => prop", NoSyn),
    42.1 --- a/src/Pure/raw_simplifier.ML	Fri Apr 08 11:39:45 2011 +0200
    42.2 +++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 13:31:16 2011 +0200
    42.3 @@ -306,7 +306,7 @@
    42.4    let
    42.5      val names = Term.declare_term_names t Name.context;
    42.6      val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
    42.7 -    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
    42.8 +    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
    42.9    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
   42.10  
   42.11  fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
    43.1 --- a/src/Pure/sign.ML	Fri Apr 08 11:39:45 2011 +0200
    43.2 +++ b/src/Pure/sign.ML	Fri Apr 08 13:31:16 2011 +0200
    43.3 @@ -477,9 +477,9 @@
    43.4  
    43.5  in
    43.6  
    43.7 -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
    43.8 +val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
    43.9  val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
   43.10 -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
   43.11 +val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
   43.12  val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
   43.13  
   43.14  end;
    44.1 --- a/src/Pure/type_infer.ML	Fri Apr 08 11:39:45 2011 +0200
    44.2 +++ b/src/Pure/type_infer.ML	Fri Apr 08 13:31:16 2011 +0200
    44.3 @@ -300,7 +300,7 @@
    44.4          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    44.5          fun prep t =
    44.6            let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
    44.7 -          in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
    44.8 +          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
    44.9        in (map prep ts', Ts') end;
   44.10  
   44.11      fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
    45.1 --- a/src/Tools/Code/code_thingol.ML	Fri Apr 08 11:39:45 2011 +0200
    45.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Apr 08 13:31:16 2011 +0200
    45.3 @@ -688,7 +688,7 @@
    45.4        pair (IVar (SOME v))
    45.5    | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
    45.6        let
    45.7 -        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
    45.8 +        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
    45.9          val v'' = if member (op =) (Term.add_free_names t' []) v'
   45.10            then SOME v' else NONE
   45.11        in
    46.1 --- a/src/Tools/induct.ML	Fri Apr 08 11:39:45 2011 +0200
    46.2 +++ b/src/Tools/induct.ML	Fri Apr 08 13:31:16 2011 +0200
    46.3 @@ -580,7 +580,7 @@
    46.4    in
    46.5      if not (null params) then
    46.6        (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
    46.7 -        commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
    46.8 +        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
    46.9        Seq.single rule)
   46.10      else
   46.11        let
    47.1 --- a/src/Tools/misc_legacy.ML	Fri Apr 08 11:39:45 2011 +0200
    47.2 +++ b/src/Tools/misc_legacy.ML	Fri Apr 08 13:31:16 2011 +0200
    47.3 @@ -61,7 +61,7 @@
    47.4  fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
    47.5        strip_context_aux (params, H :: Hs, B)
    47.6    | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
    47.7 -      let val (b, u) = Syntax.variant_abs (a, T, t)
    47.8 +      let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
    47.9        in strip_context_aux ((b, T) :: params, Hs, u) end
   47.10    | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   47.11  
    48.1 --- a/src/Tools/subtyping.ML	Fri Apr 08 11:39:45 2011 +0200
    48.2 +++ b/src/Tools/subtyping.ML	Fri Apr 08 13:31:16 2011 +0200
    48.3 @@ -200,7 +200,7 @@
    48.4      val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    48.5      fun prep t =
    48.6        let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
    48.7 -      in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
    48.8 +      in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
    48.9    in (map prep ts', Ts') end;
   48.10  
   48.11  fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);