modernized translations;
authorwenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115446c5063e4fd
parent 35114 b1fd1d756e20
child 35119 b271a8996f26
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
src/HOL/Complete_Lattice.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Inductive.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/State_Monad.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/String.thy
src/HOL/Tools/float_syntax.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/string_syntax.ML
src/HOL/Typerep.thy
src/HOLCF/Cfun.thy
src/HOLCF/Fixrec.thy
src/HOLCF/Sprod.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -106,10 +106,10 @@
     1.4    "INF x. B"     == "INF x:CONST UNIV. B"
     1.5    "INF x:A. B"   == "CONST INFI A (%x. B)"
     1.6  
     1.7 -print_translation {* [
     1.8 -Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
     1.9 -Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
    1.10 -] *} -- {* to avoid eta-contraction of body *}
    1.11 +print_translation {*
    1.12 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"},
    1.13 +    Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}]
    1.14 +*} -- {* to avoid eta-contraction of body *}
    1.15  
    1.16  context complete_lattice
    1.17  begin
    1.18 @@ -282,16 +282,16 @@
    1.19    "UNION \<equiv> SUPR"
    1.20  
    1.21  syntax
    1.22 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.23 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    1.24 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.25 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
    1.26  
    1.27  syntax (xsymbols)
    1.28 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    1.29 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    1.30 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
    1.31 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
    1.32  
    1.33  syntax (latex output)
    1.34 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.35 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.36 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.37 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.38  
    1.39  translations
    1.40    "UN x y. B"   == "UN x. UN y. B"
    1.41 @@ -308,9 +308,9 @@
    1.42    subscripts in Proof General.
    1.43  *}
    1.44  
    1.45 -print_translation {* [
    1.46 -Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
    1.47 -] *} -- {* to avoid eta-contraction of body *}
    1.48 +print_translation {*
    1.49 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
    1.50 +*} -- {* to avoid eta-contraction of body *}
    1.51  
    1.52  lemma UNION_eq_Union_image:
    1.53    "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
    1.54 @@ -518,16 +518,16 @@
    1.55    "INTER \<equiv> INFI"
    1.56  
    1.57  syntax
    1.58 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.59 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    1.60 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    1.61 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
    1.62  
    1.63  syntax (xsymbols)
    1.64 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    1.65 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    1.66 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    1.67 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
    1.68  
    1.69  syntax (latex output)
    1.70 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.71 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.72 +  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    1.73 +  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
    1.74  
    1.75  translations
    1.76    "INT x y. B"  == "INT x. INT y. B"
    1.77 @@ -535,9 +535,9 @@
    1.78    "INT x. B"    == "INT x:CONST UNIV. B"
    1.79    "INT x:A. B"  == "CONST INTER A (%x. B)"
    1.80  
    1.81 -print_translation {* [
    1.82 -Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
    1.83 -] *} -- {* to avoid eta-contraction of body *}
    1.84 +print_translation {*
    1.85 +  [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    1.86 +*} -- {* to avoid eta-contraction of body *}
    1.87  
    1.88  lemma INTER_eq_Inter_image:
    1.89    "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
     2.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 11 22:55:16 2010 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 11 23:00:22 2010 +0100
     2.3 @@ -1095,13 +1095,16 @@
     2.4  
     2.5  print_translation {*
     2.6  let
     2.7 -  fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
     2.8 -    if x<>y then raise Match
     2.9 -    else let val x' = Syntax.mark_bound x
    2.10 -             val t' = subst_bound(x',t)
    2.11 -             val P' = subst_bound(x',P)
    2.12 -         in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
    2.13 -in [("setsum", setsum_tr')] end
    2.14 +  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
    2.15 +        if x <> y then raise Match
    2.16 +        else
    2.17 +          let
    2.18 +            val x' = Syntax.mark_bound x;
    2.19 +            val t' = subst_bound (x', t);
    2.20 +            val P' = subst_bound (x', P);
    2.21 +          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
    2.22 +    | setsum_tr' _ = raise Match;
    2.23 +in [(@{const_syntax setsum}, setsum_tr')] end
    2.24  *}
    2.25  
    2.26  
     3.1 --- a/src/HOL/Fun.thy	Thu Feb 11 22:55:16 2010 +0100
     3.2 +++ b/src/HOL/Fun.thy	Thu Feb 11 23:00:22 2010 +0100
     3.3 @@ -387,18 +387,16 @@
     3.4    "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
     3.5    ""         :: "updbind => updbinds"             ("_")
     3.6    "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
     3.7 -  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000,0] 900)
     3.8 +  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000, 0] 900)
     3.9  
    3.10  translations
    3.11 -  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    3.12 -  "f(x:=y)"                     == "fun_upd f x y"
    3.13 +  "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
    3.14 +  "f(x:=y)" == "CONST fun_upd f x y"
    3.15  
    3.16  (* Hint: to define the sum of two functions (or maps), use sum_case.
    3.17           A nice infix syntax could be defined (in Datatype.thy or below) by
    3.18 -consts
    3.19 -  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    3.20 -translations
    3.21 - "fun_sum" == sum_case
    3.22 +notation
    3.23 +  sum_case  (infixr "'(+')"80)
    3.24  *)
    3.25  
    3.26  lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
     4.1 --- a/src/HOL/HOL.thy	Thu Feb 11 22:55:16 2010 +0100
     4.2 +++ b/src/HOL/HOL.thy	Thu Feb 11 23:00:22 2010 +0100
     4.3 @@ -129,16 +129,15 @@
     4.4    "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
     4.5  
     4.6  translations
     4.7 -  "THE x. P"              == "The (%x. P)"
     4.8 +  "THE x. P"              == "CONST The (%x. P)"
     4.9    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    4.10 -  "let x = a in e"        == "Let a (%x. e)"
    4.11 +  "let x = a in e"        == "CONST Let a (%x. e)"
    4.12  
    4.13  print_translation {*
    4.14 -(* To avoid eta-contraction of body: *)
    4.15 -[("The", fn [Abs abs] =>
    4.16 -     let val (x,t) = atomic_abs_tr' abs
    4.17 -     in Syntax.const "_The" $ x $ t end)]
    4.18 -*}
    4.19 +  [(@{const_syntax The}, fn [Abs abs] =>
    4.20 +      let val (x, t) = atomic_abs_tr' abs
    4.21 +      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    4.22 +*}  -- {* To avoid eta-contraction of body *}
    4.23  
    4.24  syntax (xsymbols)
    4.25    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
     5.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Feb 11 22:55:16 2010 +0100
     5.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 11 23:00:22 2010 +0100
     5.3 @@ -25,11 +25,10 @@
     5.4    "SOME x. P" == "CONST Eps (%x. P)"
     5.5  
     5.6  print_translation {*
     5.7 -(* to avoid eta-contraction of body *)
     5.8 -[(@{const_syntax Eps}, fn [Abs abs] =>
     5.9 -     let val (x,t) = atomic_abs_tr' abs
    5.10 -     in Syntax.const "_Eps" $ x $ t end)]
    5.11 -*}
    5.12 +  [(@{const_syntax Eps}, fn [Abs abs] =>
    5.13 +      let val (x, t) = atomic_abs_tr' abs
    5.14 +      in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
    5.15 +*} -- {* to avoid eta-contraction of body *}
    5.16  
    5.17  definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
    5.18  "inv_into A f == %x. SOME y. y : A & f y = x"
    5.19 @@ -315,7 +314,7 @@
    5.20  syntax
    5.21    "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
    5.22  translations
    5.23 -  "LEAST x WRT m. P" == "LeastM m (%x. P)"
    5.24 +  "LEAST x WRT m. P" == "CONST LeastM m (%x. P)"
    5.25  
    5.26  lemma LeastMI2:
    5.27    "P x ==> (!!y. P y ==> m x <= m y)
    5.28 @@ -369,11 +368,10 @@
    5.29    "Greatest == GreatestM (%x. x)"
    5.30  
    5.31  syntax
    5.32 -  "_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
    5.33 +  "_GreatestM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"
    5.34        ("GREATEST _ WRT _. _" [0, 4, 10] 10)
    5.35 -
    5.36  translations
    5.37 -  "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
    5.38 +  "GREATEST x WRT m. P" == "CONST GreatestM m (%x. P)"
    5.39  
    5.40  lemma GreatestMI2:
    5.41    "P x ==> (!!y. P y ==> m y <= m x)
     6.1 --- a/src/HOL/Inductive.thy	Thu Feb 11 22:55:16 2010 +0100
     6.2 +++ b/src/HOL/Inductive.thy	Thu Feb 11 23:00:22 2010 +0100
     6.3 @@ -301,10 +301,9 @@
     6.4    fun fun_tr ctxt [cs] =
     6.5      let
     6.6        val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     6.7 -      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr
     6.8 -                 ctxt [x, cs]
     6.9 +      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
    6.10      in lambda x ft end
    6.11 -in [("_lam_pats_syntax", fun_tr)] end
    6.12 +in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    6.13  *}
    6.14  
    6.15  end
     7.1 --- a/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 22:55:16 2010 +0100
     7.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 23:00:22 2010 +0100
     7.3 @@ -204,7 +204,7 @@
     7.4    LNil :: logic
     7.5    LCons :: logic
     7.6  translations
     7.7 -  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
     7.8 +  "case p of XCONST LNil \<Rightarrow> a | XCONST LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
     7.9  
    7.10  lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
    7.11    by (simp add: llist_case_def LNil_def
     8.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 22:55:16 2010 +0100
     8.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 23:00:22 2010 +0100
     8.3 @@ -36,8 +36,8 @@
     8.4  
     8.5  typed_print_translation {*
     8.6  let
     8.7 -  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
     8.8 -    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
     8.9 +  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
    8.10 +    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
    8.11  in [(@{const_syntax card}, card_univ_tr')]
    8.12  end
    8.13  *}
    8.14 @@ -389,7 +389,7 @@
    8.15  
    8.16  parse_translation {*
    8.17  let
    8.18 -
    8.19 +(* FIXME @{type_syntax} *)
    8.20  val num1_const = Syntax.const "Numeral_Type.num1";
    8.21  val num0_const = Syntax.const "Numeral_Type.num0";
    8.22  val B0_const = Syntax.const "Numeral_Type.bit0";
    8.23 @@ -411,7 +411,7 @@
    8.24        mk_bintype (the (Int.fromString str))
    8.25    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    8.26  
    8.27 -in [("_NumeralType", numeral_tr)] end;
    8.28 +in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
    8.29  *}
    8.30  
    8.31  print_translation {*
    8.32 @@ -419,6 +419,7 @@
    8.33  fun int_of [] = 0
    8.34    | int_of (b :: bs) = b + 2 * int_of bs;
    8.35  
    8.36 +(* FIXME @{type_syntax} *)
    8.37  fun bin_of (Const ("num0", _)) = []
    8.38    | bin_of (Const ("num1", _)) = [1]
    8.39    | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
    8.40 @@ -435,6 +436,7 @@
    8.41    end
    8.42    | bit_tr' b _ = raise Match;
    8.43  
    8.44 +(* FIXME @{type_syntax} *)
    8.45  in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
    8.46  *}
    8.47  
     9.1 --- a/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 22:55:16 2010 +0100
     9.2 +++ b/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 23:00:22 2010 +0100
     9.3 @@ -15,7 +15,7 @@
     9.4  translations
     9.5    "n" <= "CONST of_nat n"
     9.6    "n" <= "CONST int n"
     9.7 -  "n" <= "real n"
     9.8 +  "n" <= "CONST real n"
     9.9    "n" <= "CONST real_of_nat n"
    9.10    "n" <= "CONST real_of_int n"
    9.11    "n" <= "CONST of_real n"
    9.12 @@ -23,10 +23,10 @@
    9.13  
    9.14  (* append *)
    9.15  syntax (latex output)
    9.16 -  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    9.17 +  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    9.18  translations
    9.19 -  "appendL xs ys" <= "xs @ ys" 
    9.20 -  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
    9.21 +  "_appendL xs ys" <= "xs @ ys" 
    9.22 +  "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
    9.23  
    9.24  
    9.25  (* deprecated, use thm with style instead, will be removed *)
    10.1 --- a/src/HOL/Library/State_Monad.thy	Thu Feb 11 22:55:16 2010 +0100
    10.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Feb 11 23:00:22 2010 +0100
    10.3 @@ -159,15 +159,15 @@
    10.4    fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
    10.5          let
    10.6            val (v, g') = dest_abs_eta g;
    10.7 -        in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
    10.8 +        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
    10.9      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   10.10 -        Const ("_fcomp", dummyT) $ f $ unfold_monad g
   10.11 +        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
   10.12      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   10.13          let
   10.14            val (v, g') = dest_abs_eta g;
   10.15 -        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
   10.16 +        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
   10.17      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   10.18 -        Const ("return", dummyT) $ f
   10.19 +        Const (@{const_syntax "return"}, dummyT) $ f
   10.20      | unfold_monad f = f;
   10.21    fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
   10.22      | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
   10.23 @@ -175,18 +175,23 @@
   10.24      | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   10.25          contains_scomp t;
   10.26    fun scomp_monad_tr' (f::g::ts) = list_comb
   10.27 -    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
   10.28 -  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
   10.29 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
   10.30 +    (Const (@{syntax_const "_do"}, dummyT) $
   10.31 +      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
   10.32 +  fun fcomp_monad_tr' (f::g::ts) =
   10.33 +    if contains_scomp g then list_comb
   10.34 +      (Const (@{syntax_const "_do"}, dummyT) $
   10.35 +        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
   10.36      else raise Match;
   10.37 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
   10.38 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   10.39 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   10.40 +    if contains_scomp g' then list_comb
   10.41 +      (Const (@{syntax_const "_do"}, dummyT) $
   10.42 +        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   10.43      else raise Match;
   10.44 -in [
   10.45 -  (@{const_syntax scomp}, scomp_monad_tr'),
   10.46 +in
   10.47 + [(@{const_syntax scomp}, scomp_monad_tr'),
   10.48    (@{const_syntax fcomp}, fcomp_monad_tr'),
   10.49 -  (@{const_syntax Let}, Let_monad_tr')
   10.50 -] end;
   10.51 +  (@{const_syntax Let}, Let_monad_tr')]
   10.52 +end;
   10.53  *}
   10.54  
   10.55  text {*
    11.1 --- a/src/HOL/List.thy	Thu Feb 11 22:55:16 2010 +0100
    11.2 +++ b/src/HOL/List.thy	Thu Feb 11 23:00:22 2010 +0100
    11.3 @@ -15,13 +15,14 @@
    11.4  
    11.5  syntax
    11.6    -- {* list Enumeration *}
    11.7 -  "@list" :: "args => 'a list"    ("[(_)]")
    11.8 +  "_list" :: "args => 'a list"    ("[(_)]")
    11.9  
   11.10  translations
   11.11    "[x, xs]" == "x#[xs]"
   11.12    "[x]" == "x#[]"
   11.13  
   11.14 -subsection{*Basic list processing functions*}
   11.15 +
   11.16 +subsection {* Basic list processing functions *}
   11.17  
   11.18  primrec
   11.19    hd :: "'a list \<Rightarrow> 'a" where
   11.20 @@ -68,15 +69,15 @@
   11.21  
   11.22  syntax
   11.23    -- {* Special syntax for filter *}
   11.24 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
   11.25 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
   11.26  
   11.27  translations
   11.28    "[x<-xs . P]"== "CONST filter (%x. P) xs"
   11.29  
   11.30  syntax (xsymbols)
   11.31 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   11.32 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   11.33  syntax (HTML output)
   11.34 -  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   11.35 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   11.36  
   11.37  primrec
   11.38    foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
   11.39 @@ -132,7 +133,7 @@
   11.40    "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
   11.41  
   11.42  translations
   11.43 -  "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
   11.44 +  "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   11.45    "xs[i:=x]" == "CONST list_update xs i x"
   11.46  
   11.47  primrec
   11.48 @@ -363,45 +364,52 @@
   11.49    val mapC = Syntax.const @{const_name map};
   11.50    val concatC = Syntax.const @{const_name concat};
   11.51    val IfC = Syntax.const @{const_name If};
   11.52 +
   11.53    fun singl x = ConsC $ x $ NilC;
   11.54  
   11.55 -   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   11.56 +  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   11.57      let
   11.58        val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
   11.59        val e = if opti then singl e else e;
   11.60 -      val case1 = Syntax.const "_case1" $ p $ e;
   11.61 -      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
   11.62 -                                        $ NilC;
   11.63 -      val cs = Syntax.const "_case2" $ case1 $ case2
   11.64 -      val ft = Datatype_Case.case_tr false Datatype.info_of_constr
   11.65 -                 ctxt [x, cs]
   11.66 +      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
   11.67 +      val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC;
   11.68 +      val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   11.69 +      val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
   11.70      in lambda x ft end;
   11.71  
   11.72    fun abs_tr ctxt (p as Free(s,T)) e opti =
   11.73 -        let val thy = ProofContext.theory_of ctxt;
   11.74 -            val s' = Sign.intern_const thy s
   11.75 -        in if Sign.declared_const thy s'
   11.76 -           then (pat_tr ctxt p e opti, false)
   11.77 -           else (lambda p e, true)
   11.78 +        let
   11.79 +          val thy = ProofContext.theory_of ctxt;
   11.80 +          val s' = Sign.intern_const thy s;
   11.81 +        in
   11.82 +          if Sign.declared_const thy s'
   11.83 +          then (pat_tr ctxt p e opti, false)
   11.84 +          else (lambda p e, true)
   11.85          end
   11.86      | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
   11.87  
   11.88 -  fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
   11.89 -        let val res = case qs of Const("_lc_end",_) => singl e
   11.90 -                      | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
   11.91 +  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   11.92 +        let
   11.93 +          val res =
   11.94 +            (case qs of
   11.95 +              Const (@{syntax_const "_lc_end"}, _) => singl e
   11.96 +            | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   11.97          in IfC $ b $ res $ NilC end
   11.98 -    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
   11.99 +    | lc_tr ctxt
  11.100 +          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
  11.101 +            Const(@{syntax_const "_lc_end"}, _)] =
  11.102          (case abs_tr ctxt p e true of
  11.103 -           (f,true) => mapC $ f $ es
  11.104 -         | (f, false) => concatC $ (mapC $ f $ es))
  11.105 -    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
  11.106 -        let val e' = lc_tr ctxt [e,q,qs];
  11.107 -        in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
  11.108 -
  11.109 -in [("_listcompr", lc_tr)] end
  11.110 +          (f, true) => mapC $ f $ es
  11.111 +        | (f, false) => concatC $ (mapC $ f $ es))
  11.112 +    | lc_tr ctxt
  11.113 +          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
  11.114 +            Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
  11.115 +        let val e' = lc_tr ctxt [e, q, qs];
  11.116 +        in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
  11.117 +
  11.118 +in [(@{syntax_const "_listcompr"}, lc_tr)] end
  11.119  *}
  11.120  
  11.121 -(*
  11.122  term "[(x,y,z). b]"
  11.123  term "[(x,y,z). x\<leftarrow>xs]"
  11.124  term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
  11.125 @@ -418,9 +426,11 @@
  11.126  term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
  11.127  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
  11.128  term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
  11.129 +(*
  11.130  term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
  11.131  *)
  11.132  
  11.133 +
  11.134  subsubsection {* @{const Nil} and @{const Cons} *}
  11.135  
  11.136  lemma not_Cons_self [simp]:
  11.137 @@ -1019,6 +1029,7 @@
  11.138    "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
  11.139    by (induct xs) auto
  11.140  
  11.141 +
  11.142  subsubsection {* @{text filter} *}
  11.143  
  11.144  lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
  11.145 @@ -1200,6 +1211,7 @@
  11.146  
  11.147  declare partition.simps[simp del]
  11.148  
  11.149 +
  11.150  subsubsection {* @{text concat} *}
  11.151  
  11.152  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
  11.153 @@ -2074,6 +2086,7 @@
  11.154    qed simp
  11.155  qed simp
  11.156  
  11.157 +
  11.158  subsubsection {* @{text list_all2} *}
  11.159  
  11.160  lemma list_all2_lengthD [intro?]: 
  11.161 @@ -2413,6 +2426,7 @@
  11.162    unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
  11.163      by (simp add: sup_commute)
  11.164  
  11.165 +
  11.166  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  11.167  
  11.168  lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
  11.169 @@ -2835,6 +2849,7 @@
  11.170    from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
  11.171  qed
  11.172  
  11.173 +
  11.174  subsubsection {* @{const insert} *}
  11.175  
  11.176  lemma in_set_insert [simp]:
  11.177 @@ -3254,7 +3269,8 @@
  11.178   apply auto
  11.179  done
  11.180  
  11.181 -subsubsection{*Transpose*}
  11.182 +
  11.183 +subsubsection {* Transpose *}
  11.184  
  11.185  function transpose where
  11.186  "transpose []             = []" |
  11.187 @@ -3366,6 +3382,7 @@
  11.188      by (simp add: nth_transpose filter_map comp_def)
  11.189  qed
  11.190  
  11.191 +
  11.192  subsubsection {* (In)finiteness *}
  11.193  
  11.194  lemma finite_maxlen:
  11.195 @@ -3407,7 +3424,7 @@
  11.196  done
  11.197  
  11.198  
  11.199 -subsection {*Sorting*}
  11.200 +subsection {* Sorting *}
  11.201  
  11.202  text{* Currently it is not shown that @{const sort} returns a
  11.203  permutation of its input because the nicest proof is via multisets,
  11.204 @@ -3626,7 +3643,8 @@
  11.205  apply(simp add:sorted_Cons)
  11.206  done
  11.207  
  11.208 -subsubsection {*@{const transpose} on sorted lists*}
  11.209 +
  11.210 +subsubsection {* @{const transpose} on sorted lists *}
  11.211  
  11.212  lemma sorted_transpose[simp]:
  11.213    shows "sorted (rev (map length (transpose xs)))"
  11.214 @@ -3774,6 +3792,7 @@
  11.215      by (auto simp: nth_transpose intro: nth_equalityI)
  11.216  qed
  11.217  
  11.218 +
  11.219  subsubsection {* @{text sorted_list_of_set} *}
  11.220  
  11.221  text{* This function maps (finite) linearly ordered sets to sorted
  11.222 @@ -3805,6 +3824,7 @@
  11.223  
  11.224  end
  11.225  
  11.226 +
  11.227  subsubsection {* @{text lists}: the list-forming operator over sets *}
  11.228  
  11.229  inductive_set
  11.230 @@ -3864,8 +3884,7 @@
  11.231  by auto
  11.232  
  11.233  
  11.234 -
  11.235 -subsubsection{* Inductive definition for membership *}
  11.236 +subsubsection {* Inductive definition for membership *}
  11.237  
  11.238  inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  11.239  where
  11.240 @@ -3881,8 +3900,7 @@
  11.241  done
  11.242  
  11.243  
  11.244 -
  11.245 -subsubsection{*Lists as Cartesian products*}
  11.246 +subsubsection {* Lists as Cartesian products *}
  11.247  
  11.248  text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  11.249  @{term A} and tail drawn from @{term Xs}.*}
  11.250 @@ -3903,7 +3921,7 @@
  11.251    |  "listset (A # As) = set_Cons A (listset As)"
  11.252  
  11.253  
  11.254 -subsection{*Relations on Lists*}
  11.255 +subsection {* Relations on Lists *}
  11.256  
  11.257  subsubsection {* Length Lexicographic Ordering *}
  11.258  
  11.259 @@ -4108,7 +4126,7 @@
  11.260  by auto
  11.261  
  11.262  
  11.263 -subsubsection{*Lifting a Relation on List Elements to the Lists*}
  11.264 +subsubsection {* Lifting a Relation on List Elements to the Lists *}
  11.265  
  11.266  inductive_set
  11.267    listrel :: "('a * 'a)set => ('a list * 'a list)set"
    12.1 --- a/src/HOL/Map.thy	Thu Feb 11 22:55:16 2010 +0100
    12.2 +++ b/src/HOL/Map.thy	Thu Feb 11 23:00:22 2010 +0100
    12.3 @@ -68,7 +68,7 @@
    12.4  
    12.5  translations
    12.6    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    12.7 -  "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    12.8 +  "_MapUpd m (_maplet  x y)"    == "m(x := CONST Some y)"
    12.9    "_Map ms"                     == "_MapUpd (CONST empty) ms"
   12.10    "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
   12.11    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    13.1 --- a/src/HOL/Orderings.thy	Thu Feb 11 22:55:16 2010 +0100
    13.2 +++ b/src/HOL/Orderings.thy	Thu Feb 11 23:00:22 2010 +0100
    13.3 @@ -646,25 +646,30 @@
    13.4    val less_eq = @{const_syntax less_eq};
    13.5  
    13.6    val trans =
    13.7 -   [((All_binder, impl, less), ("_All_less", "_All_greater")),
    13.8 -    ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
    13.9 -    ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
   13.10 -    ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
   13.11 +   [((All_binder, impl, less),
   13.12 +    (@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})),
   13.13 +    ((All_binder, impl, less_eq),
   13.14 +    (@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})),
   13.15 +    ((Ex_binder, conj, less),
   13.16 +    (@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})),
   13.17 +    ((Ex_binder, conj, less_eq),
   13.18 +    (@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))];
   13.19  
   13.20 -  fun matches_bound v t = 
   13.21 -     case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
   13.22 -              | _ => false
   13.23 -  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
   13.24 -  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
   13.25 +  fun matches_bound v t =
   13.26 +    (case t of
   13.27 +      Const ("_bound", _) $ Free (v', _) => v = v'
   13.28 +    | _ => false);
   13.29 +  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
   13.30 +  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
   13.31  
   13.32    fun tr' q = (q,
   13.33      fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
   13.34 -      (case AList.lookup (op =) trans (q, c, d) of
   13.35 -        NONE => raise Match
   13.36 -      | SOME (l, g) =>
   13.37 -          if matches_bound v t andalso not (contains_var v u) then mk v l u P
   13.38 -          else if matches_bound v u andalso not (contains_var v t) then mk v g t P
   13.39 -          else raise Match)
   13.40 +        (case AList.lookup (op =) trans (q, c, d) of
   13.41 +          NONE => raise Match
   13.42 +        | SOME (l, g) =>
   13.43 +            if matches_bound v t andalso not (contains_var v u) then mk v l u P
   13.44 +            else if matches_bound v u andalso not (contains_var v t) then mk v g t P
   13.45 +            else raise Match)
   13.46       | _ => raise Match);
   13.47  in [tr' All_binder, tr' Ex_binder] end
   13.48  *}
    14.1 --- a/src/HOL/Product_Type.thy	Thu Feb 11 22:55:16 2010 +0100
    14.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 11 23:00:22 2010 +0100
    14.3 @@ -180,65 +180,81 @@
    14.4    "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
    14.5  
    14.6  translations
    14.7 -  "(x, y)"       == "Pair x y"
    14.8 +  "(x, y)" == "CONST Pair x y"
    14.9    "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   14.10 -  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
   14.11 -  "%(x,y).b"     == "split(%x y. b)"
   14.12 -  "_abs (Pair x y) t" => "%(x,y).t"
   14.13 +  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
   14.14 +  "%(x, y). b" == "CONST split (%x y. b)"
   14.15 +  "_abs (CONST Pair x y) t" => "%(x, y). t"
   14.16    (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   14.17       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
   14.18  
   14.19 -(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
   14.20 -(* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
   14.21 +(*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
   14.22 +  works best with enclosing "let", if "let" does not avoid eta-contraction*)
   14.23  print_translation {*
   14.24 -let fun split_tr' [Abs (x,T,t as (Abs abs))] =
   14.25 -      (* split (%x y. t) => %(x,y) t *)
   14.26 -      let val (y,t') = atomic_abs_tr' abs;
   14.27 -          val (x',t'') = atomic_abs_tr' (x,T,t');
   14.28 -    
   14.29 -      in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
   14.30 -    | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
   14.31 -       (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   14.32 -       let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
   14.33 -           val (x',t'') = atomic_abs_tr' (x,T,t');
   14.34 -       in Syntax.const "_abs"$ 
   14.35 -           (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
   14.36 -    | split_tr' [Const ("split",_)$t] =
   14.37 -       (* split (split (%x y z. t)) => %((x,y),z). t *)   
   14.38 -       split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   14.39 -    | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
   14.40 -       (* split (%pttrn z. t) => %(pttrn,z). t *)
   14.41 -       let val (z,t) = atomic_abs_tr' abs;
   14.42 -       in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
   14.43 -    | split_tr' _ =  raise Match;
   14.44 -in [("split", split_tr')]
   14.45 -end
   14.46 +let
   14.47 +  fun split_tr' [Abs (x, T, t as (Abs abs))] =
   14.48 +        (* split (%x y. t) => %(x,y) t *)
   14.49 +        let
   14.50 +          val (y, t') = atomic_abs_tr' abs;
   14.51 +          val (x', t'') = atomic_abs_tr' (x, T, t');
   14.52 +        in
   14.53 +          Syntax.const @{syntax_const "_abs"} $
   14.54 +            (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   14.55 +        end
   14.56 +    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
   14.57 +        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   14.58 +        let
   14.59 +          val Const (@{syntax_const "_abs"}, _) $
   14.60 +            (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
   14.61 +          val (x', t'') = atomic_abs_tr' (x, T, t');
   14.62 +        in
   14.63 +          Syntax.const @{syntax_const "_abs"} $
   14.64 +            (Syntax.const @{syntax_const "_pattern"} $ x' $
   14.65 +              (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
   14.66 +        end
   14.67 +    | split_tr' [Const (@{const_syntax split}, _) $ t] =
   14.68 +        (* split (split (%x y z. t)) => %((x, y), z). t *)
   14.69 +        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   14.70 +    | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   14.71 +        (* split (%pttrn z. t) => %(pttrn,z). t *)
   14.72 +        let val (z, t) = atomic_abs_tr' abs in
   14.73 +          Syntax.const @{syntax_const "_abs"} $
   14.74 +            (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   14.75 +        end
   14.76 +    | split_tr' _ = raise Match;
   14.77 +in [(@{const_syntax split}, split_tr')] end
   14.78  *}
   14.79  
   14.80  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   14.81  typed_print_translation {*
   14.82  let
   14.83 -  fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
   14.84 -    | split_guess_names_tr' _ T  [Abs (x,xT,t)] =
   14.85 +  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
   14.86 +    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
   14.87          (case (head_of t) of
   14.88 -           Const ("split",_) => raise Match
   14.89 -         | _ => let 
   14.90 -                  val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
   14.91 -                  val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)$Bound 0); 
   14.92 -                  val (x',t'') = atomic_abs_tr' (x,xT,t');
   14.93 -                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
   14.94 +          Const (@{const_syntax split}, _) => raise Match
   14.95 +        | _ =>
   14.96 +          let 
   14.97 +            val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   14.98 +            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
   14.99 +            val (x', t'') = atomic_abs_tr' (x, xT, t');
  14.100 +          in
  14.101 +            Syntax.const @{syntax_const "_abs"} $
  14.102 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
  14.103 +          end)
  14.104      | split_guess_names_tr' _ T [t] =
  14.105 -       (case (head_of t) of
  14.106 -           Const ("split",_) => raise Match 
  14.107 -         | _ => let 
  14.108 -                  val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
  14.109 -                  val (y,t') = 
  14.110 -                        atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)$Bound 1$Bound 0); 
  14.111 -                  val (x',t'') = atomic_abs_tr' ("x",xT,t');
  14.112 -                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
  14.113 +        (case head_of t of
  14.114 +          Const (@{const_syntax split}, _) => raise Match
  14.115 +        | _ =>
  14.116 +          let
  14.117 +            val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
  14.118 +            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
  14.119 +            val (x', t'') = atomic_abs_tr' ("x", xT, t');
  14.120 +          in
  14.121 +            Syntax.const @{syntax_const "_abs"} $
  14.122 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
  14.123 +          end)
  14.124      | split_guess_names_tr' _ _ _ = raise Match;
  14.125 -in [("split", split_guess_names_tr')]
  14.126 -end 
  14.127 +in [(@{const_syntax split}, split_guess_names_tr')] end
  14.128  *}
  14.129  
  14.130  
  14.131 @@ -855,10 +871,9 @@
  14.132    Times  (infixr "\<times>" 80)
  14.133  
  14.134  syntax
  14.135 -  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
  14.136 -
  14.137 +  "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
  14.138  translations
  14.139 -  "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)"
  14.140 +  "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
  14.141  
  14.142  lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
  14.143    by (unfold Sigma_def) blast
    15.1 --- a/src/HOL/Set.thy	Thu Feb 11 22:55:16 2010 +0100
    15.2 +++ b/src/HOL/Set.thy	Thu Feb 11 23:00:22 2010 +0100
    15.3 @@ -48,20 +48,16 @@
    15.4  text {* Set comprehensions *}
    15.5  
    15.6  syntax
    15.7 -  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
    15.8 -
    15.9 +  "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
   15.10  translations
   15.11 -  "{x. P}"      == "Collect (%x. P)"
   15.12 +  "{x. P}" == "CONST Collect (%x. P)"
   15.13  
   15.14  syntax
   15.15 -  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
   15.16 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
   15.17 -
   15.18 +  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
   15.19  syntax (xsymbols)
   15.20 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
   15.21 -
   15.22 +  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
   15.23  translations
   15.24 -  "{x:A. P}"    => "{x. x:A & P}"
   15.25 +  "{x:A. P}" => "{x. x:A & P}"
   15.26  
   15.27  lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
   15.28    by (simp add: Collect_def mem_def)
   15.29 @@ -107,11 +103,10 @@
   15.30    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
   15.31  
   15.32  syntax
   15.33 -  "@Finset"     :: "args => 'a set"                       ("{(_)}")
   15.34 -
   15.35 +  "_Finset" :: "args => 'a set"    ("{(_)}")
   15.36  translations
   15.37 -  "{x, xs}"     == "CONST insert x {xs}"
   15.38 -  "{x}"         == "CONST insert x {}"
   15.39 +  "{x, xs}" == "CONST insert x {xs}"
   15.40 +  "{x}" == "CONST insert x {}"
   15.41  
   15.42  
   15.43  subsection {* Subsets and bounded quantifiers *}
   15.44 @@ -191,9 +186,9 @@
   15.45    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   15.46  
   15.47  translations
   15.48 -  "ALL x:A. P"  == "Ball A (%x. P)"
   15.49 -  "EX x:A. P"   == "Bex A (%x. P)"
   15.50 -  "EX! x:A. P"  => "EX! x. x:A & P"
   15.51 +  "ALL x:A. P" == "CONST Ball A (%x. P)"
   15.52 +  "EX x:A. P" == "CONST Bex A (%x. P)"
   15.53 +  "EX! x:A. P" => "EX! x. x:A & P"
   15.54    "LEAST x:A. P" => "LEAST x. x:A & P"
   15.55  
   15.56  syntax (output)
   15.57 @@ -233,31 +228,34 @@
   15.58  
   15.59  print_translation {*
   15.60  let
   15.61 -  val Type (set_type, _) = @{typ "'a set"};
   15.62 -  val All_binder = Syntax.binder_name @{const_syntax "All"};
   15.63 -  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
   15.64 +  val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
   15.65 +  val All_binder = Syntax.binder_name @{const_syntax All};
   15.66 +  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   15.67    val impl = @{const_syntax "op -->"};
   15.68    val conj = @{const_syntax "op &"};
   15.69 -  val sbset = @{const_syntax "subset"};
   15.70 -  val sbset_eq = @{const_syntax "subset_eq"};
   15.71 +  val sbset = @{const_syntax subset};
   15.72 +  val sbset_eq = @{const_syntax subset_eq};
   15.73  
   15.74    val trans =
   15.75 -   [((All_binder, impl, sbset), "_setlessAll"),
   15.76 -    ((All_binder, impl, sbset_eq), "_setleAll"),
   15.77 -    ((Ex_binder, conj, sbset), "_setlessEx"),
   15.78 -    ((Ex_binder, conj, sbset_eq), "_setleEx")];
   15.79 +   [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
   15.80 +    ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
   15.81 +    ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
   15.82 +    ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
   15.83  
   15.84    fun mk v v' c n P =
   15.85      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
   15.86      then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
   15.87  
   15.88    fun tr' q = (q,
   15.89 -    fn [Const ("_bound", _) $ Free (v, Type (T, _)), Const (c, _) $ (Const (d, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =>
   15.90 -         if T = (set_type) then case AList.lookup (op =) trans (q, c, d)
   15.91 -          of NONE => raise Match
   15.92 -           | SOME l => mk v v' l n P
   15.93 -         else raise Match
   15.94 -     | _ => raise Match);
   15.95 +        fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
   15.96 +            Const (c, _) $
   15.97 +              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
   15.98 +            if T = set_type then
   15.99 +              (case AList.lookup (op =) trans (q, c, d) of
  15.100 +                NONE => raise Match
  15.101 +              | SOME l => mk v v' l n P)
  15.102 +            else raise Match
  15.103 +         | _ => raise Match);
  15.104  in
  15.105    [tr' All_binder, tr' Ex_binder]
  15.106  end
  15.107 @@ -270,55 +268,63 @@
  15.108    only translated if @{text "[0..n] subset bvs(e)"}.
  15.109  *}
  15.110  
  15.111 +syntax
  15.112 +  "_Setcompr" :: "'a => idts => bool => 'a set"    ("(1{_ |/_./ _})")
  15.113 +
  15.114  parse_translation {*
  15.115    let
  15.116 -    val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
  15.117 +    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
  15.118  
  15.119 -    fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
  15.120 +    fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
  15.121        | nvars _ = 1;
  15.122  
  15.123      fun setcompr_tr [e, idts, b] =
  15.124        let
  15.125 -        val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
  15.126 -        val P = Syntax.const "op &" $ eq $ b;
  15.127 +        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
  15.128 +        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
  15.129          val exP = ex_tr [idts, P];
  15.130 -      in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end;
  15.131 +      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
  15.132  
  15.133 -  in [("@SetCompr", setcompr_tr)] end;
  15.134 +  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
  15.135  *}
  15.136  
  15.137 -print_translation {* [
  15.138 -Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
  15.139 -Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
  15.140 -] *} -- {* to avoid eta-contraction of body *}
  15.141 +print_translation {*
  15.142 + [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
  15.143 +  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
  15.144 +*} -- {* to avoid eta-contraction of body *}
  15.145  
  15.146  print_translation {*
  15.147  let
  15.148 -  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
  15.149 +  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
  15.150  
  15.151    fun setcompr_tr' [Abs (abs as (_, _, P))] =
  15.152      let
  15.153 -      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
  15.154 -        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
  15.155 +      fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
  15.156 +        | check (Const (@{const_syntax "op &"}, _) $
  15.157 +              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
  15.158              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
  15.159              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
  15.160 -        | check _ = false
  15.161 +        | check _ = false;
  15.162  
  15.163          fun tr' (_ $ abs) =
  15.164            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
  15.165 -          in Syntax.const "@SetCompr" $ e $ idts $ Q end;
  15.166 -    in if check (P, 0) then tr' P
  15.167 -       else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs
  15.168 -                val M = Syntax.const "@Coll" $ x $ t
  15.169 -            in case t of
  15.170 -                 Const("op &",_)
  15.171 -                   $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A)
  15.172 -                   $ P =>
  15.173 -                   if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M
  15.174 -               | _ => M
  15.175 -            end
  15.176 +          in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
  15.177 +    in
  15.178 +      if check (P, 0) then tr' P
  15.179 +      else
  15.180 +        let
  15.181 +          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
  15.182 +          val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
  15.183 +        in
  15.184 +          case t of
  15.185 +            Const (@{const_syntax "op &"}, _) $
  15.186 +              (Const (@{const_syntax "op :"}, _) $
  15.187 +                (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
  15.188 +            if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
  15.189 +          | _ => M
  15.190 +        end
  15.191      end;
  15.192 -  in [("Collect", setcompr_tr')] end;
  15.193 +  in [(@{const_syntax Collect}, setcompr_tr')] end;
  15.194  *}
  15.195  
  15.196  setup {*
    16.1 --- a/src/HOL/SetInterval.thy	Thu Feb 11 22:55:16 2010 +0100
    16.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 11 23:00:22 2010 +0100
    16.3 @@ -54,22 +54,22 @@
    16.4  @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
    16.5  
    16.6  syntax
    16.7 -  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
    16.8 -  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
    16.9 -  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
   16.10 -  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
   16.11 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
   16.12 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
   16.13 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
   16.14 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
   16.15  
   16.16  syntax (xsymbols)
   16.17 -  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
   16.18 -  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
   16.19 -  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
   16.20 -  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
   16.21 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
   16.22 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
   16.23 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
   16.24 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
   16.25  
   16.26  syntax (latex output)
   16.27 -  "@UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
   16.28 -  "@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
   16.29 -  "@INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
   16.30 -  "@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
   16.31 +  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
   16.32 +  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
   16.33 +  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
   16.34 +  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
   16.35  
   16.36  translations
   16.37    "UN i<=n. A"  == "UN i:{..n}. A"
    17.1 --- a/src/HOL/String.thy	Thu Feb 11 22:55:16 2010 +0100
    17.2 +++ b/src/HOL/String.thy	Thu Feb 11 23:00:22 2010 +0100
    17.3 @@ -5,7 +5,7 @@
    17.4  theory String
    17.5  imports List
    17.6  uses
    17.7 -  "Tools/string_syntax.ML"
    17.8 +  ("Tools/string_syntax.ML")
    17.9    ("Tools/string_code.ML")
   17.10  begin
   17.11  
   17.12 @@ -78,6 +78,7 @@
   17.13  syntax
   17.14    "_String" :: "xstr => string"    ("_")
   17.15  
   17.16 +use "Tools/string_syntax.ML"
   17.17  setup StringSyntax.setup
   17.18  
   17.19  definition chars :: string where
    18.1 --- a/src/HOL/Tools/float_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
    18.2 +++ b/src/HOL/Tools/float_syntax.ML	Thu Feb 11 23:00:22 2010 +0100
    18.3 @@ -1,7 +1,6 @@
    18.4 -(*  ID:         $Id$
    18.5 -    Authors:    Tobias Nipkow, TU Muenchen
    18.6 +(*  Author:     Tobias Nipkow, TU Muenchen
    18.7  
    18.8 -Concrete syntax for floats
    18.9 +Concrete syntax for floats.
   18.10  *)
   18.11  
   18.12  signature FLOAT_SYNTAX =
   18.13 @@ -18,19 +17,21 @@
   18.14  
   18.15  fun mk_number i =
   18.16    let
   18.17 -    fun mk 0 = Syntax.const @{const_name Int.Pls}
   18.18 -      | mk ~1 =  Syntax.const @{const_name Int.Min}
   18.19 -      | mk i = let val (q, r) = Integer.div_mod i 2
   18.20 -               in HOLogic.mk_bit r $ (mk q) end;
   18.21 -  in Syntax.const @{const_name Int.number_of} $ mk i end;
   18.22 +    fun mk 0 = Syntax.const @{const_syntax Int.Pls}
   18.23 +      | mk ~1 = Syntax.const @{const_syntax Int.Min}
   18.24 +      | mk i =
   18.25 +          let val (q, r) = Integer.div_mod i 2
   18.26 +          in HOLogic.mk_bit r $ (mk q) end;
   18.27 +  in Syntax.const @{const_syntax Int.number_of} $ mk i end;
   18.28  
   18.29  fun mk_frac str =
   18.30    let
   18.31 -    val {mant=i, exp = n} = Syntax.read_float str;
   18.32 -    val exp = Syntax.const @{const_name Power.power};
   18.33 +    val {mant = i, exp = n} = Syntax.read_float str;
   18.34 +    val exp = Syntax.const @{const_syntax Power.power};
   18.35      val ten = mk_number 10;
   18.36 -    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
   18.37 -  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
   18.38 +    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
   18.39 +  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
   18.40 +
   18.41  in
   18.42  
   18.43  fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
   18.44 @@ -42,6 +43,6 @@
   18.45  (* theory setup *)
   18.46  
   18.47  val setup =
   18.48 -  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
   18.49 +  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
   18.50  
   18.51  end;
    19.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
    19.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 23:00:22 2010 +0100
    19.3 @@ -27,7 +27,7 @@
    19.4  in
    19.5  
    19.6  fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
    19.7 -      Syntax.const @{const_name Int.number_of} $ mk_bin num
    19.8 +      Syntax.const @{const_syntax Int.number_of} $ mk_bin num
    19.9    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
   19.10  
   19.11  end;
   19.12 @@ -37,10 +37,10 @@
   19.13  
   19.14  local
   19.15  
   19.16 -fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
   19.17 -  | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
   19.18 -  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
   19.19 -  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
   19.20 +fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = []
   19.21 +  | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1]
   19.22 +  | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs
   19.23 +  | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs
   19.24    | dest_bin _ = raise Match;
   19.25  
   19.26  fun leading _ [] = 0
   19.27 @@ -64,11 +64,12 @@
   19.28    end;
   19.29  
   19.30  fun syntax_numeral t =
   19.31 -  Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
   19.32 +  Syntax.const @{syntax_const "_Numeral"} $
   19.33 +    (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
   19.34  
   19.35  in
   19.36  
   19.37 -fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
   19.38 +fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =  (* FIXME @{type_syntax} *)
   19.39        let val t' =
   19.40          if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
   19.41          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
   19.42 @@ -84,7 +85,7 @@
   19.43  (* theory setup *)
   19.44  
   19.45  val setup =
   19.46 -  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
   19.47 +  Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
   19.48    Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
   19.49  
   19.50  end;
    20.1 --- a/src/HOL/Tools/string_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
    20.2 +++ b/src/HOL/Tools/string_syntax.ML	Thu Feb 11 23:00:22 2010 +0100
    20.3 @@ -30,7 +30,7 @@
    20.4  
    20.5  fun mk_char s =
    20.6    if Symbol.is_ascii s then
    20.7 -    Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    20.8 +    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    20.9    else error ("Non-ASCII symbol: " ^ quote s);
   20.10  
   20.11  val specials = explode "\\\"`'";
   20.12 @@ -41,11 +41,13 @@
   20.13      then c else raise Match
   20.14    end;
   20.15  
   20.16 -fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
   20.17 +fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   20.18    | dest_char _ = raise Match;
   20.19  
   20.20  fun syntax_string cs =
   20.21 -  Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
   20.22 +  Syntax.Appl
   20.23 +    [Syntax.Constant @{syntax_const "_inner_string"},
   20.24 +      Syntax.Variable (Syntax.implode_xstr cs)];
   20.25  
   20.26  
   20.27  fun char_ast_tr [Syntax.Variable xstr] =
   20.28 @@ -54,24 +56,29 @@
   20.29      | _ => error ("Single character expected: " ^ xstr))
   20.30    | char_ast_tr asts = raise AST ("char_ast_tr", asts);
   20.31  
   20.32 -fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
   20.33 +fun char_ast_tr' [c1, c2] =
   20.34 +      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
   20.35    | char_ast_tr' _ = raise Match;
   20.36  
   20.37  
   20.38  (* string *)
   20.39  
   20.40 -fun mk_string [] = Syntax.Constant "Nil"
   20.41 -  | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
   20.42 +fun mk_string [] = Syntax.Constant @{const_syntax Nil}
   20.43 +  | mk_string (c :: cs) =
   20.44 +      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
   20.45  
   20.46  fun string_ast_tr [Syntax.Variable xstr] =
   20.47      (case Syntax.explode_xstr xstr of
   20.48 -      [] => Syntax.Appl
   20.49 -        [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
   20.50 +      [] =>
   20.51 +        Syntax.Appl
   20.52 +          [Syntax.Constant Syntax.constrainC,
   20.53 +            Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"]  (* FIXME @{type_syntax} *)
   20.54      | cs => mk_string cs)
   20.55    | string_ast_tr asts = raise AST ("string_tr", asts);
   20.56  
   20.57 -fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
   20.58 -        syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
   20.59 +fun list_ast_tr' [args] =
   20.60 +      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
   20.61 +        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
   20.62    | list_ast_tr' ts = raise Match;
   20.63  
   20.64  
   20.65 @@ -79,7 +86,7 @@
   20.66  
   20.67  val setup =
   20.68    Sign.add_trfuns
   20.69 -    ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
   20.70 -      [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
   20.71 +   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
   20.72 +    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
   20.73  
   20.74  end;
    21.1 --- a/src/HOL/Typerep.thy	Thu Feb 11 22:55:16 2010 +0100
    21.2 +++ b/src/HOL/Typerep.thy	Thu Feb 11 23:00:22 2010 +0100
    21.3 @@ -17,22 +17,27 @@
    21.4  
    21.5  end
    21.6  
    21.7 -setup {*
    21.8 +syntax
    21.9 +  "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
   21.10 +
   21.11 +parse_translation {*
   21.12  let
   21.13    fun typerep_tr (*"_TYPEREP"*) [ty] =
   21.14 -        Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
   21.15 -          (Lexicon.const "itself" $ ty))
   21.16 +        Syntax.const @{const_syntax typerep} $
   21.17 +          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
   21.18 +            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
   21.19      | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
   21.20 -  fun typerep_tr' show_sorts (*"typerep"*)
   21.21 +in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
   21.22 +*}
   21.23 +
   21.24 +typed_print_translation {*
   21.25 +let
   21.26 +  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
   21.27            (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
   21.28 -        Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
   21.29 +        Term.list_comb
   21.30 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
   21.31      | typerep_tr' _ T ts = raise Match;
   21.32 -in
   21.33 -  Sign.add_syntax_i
   21.34 -    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
   21.35 -  #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
   21.36 -  #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
   21.37 -end
   21.38 +in [(@{const_syntax typerep}, typerep_tr')] end
   21.39  *}
   21.40  
   21.41  setup {*
    22.1 --- a/src/HOLCF/Cfun.thy	Thu Feb 11 22:55:16 2010 +0100
    22.2 +++ b/src/HOLCF/Cfun.thy	Thu Feb 11 23:00:22 2010 +0100
    22.3 @@ -40,8 +40,8 @@
    22.4  syntax "_cabs" :: "'a"
    22.5  
    22.6  parse_translation {*
    22.7 -(* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
    22.8 -  [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
    22.9 +(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
   22.10 +  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
   22.11  *}
   22.12  
   22.13  text {* To avoid eta-contraction of body: *}
   22.14 @@ -49,13 +49,13 @@
   22.15    let
   22.16      fun cabs_tr' _ _ [Abs abs] = let
   22.17            val (x,t) = atomic_abs_tr' abs
   22.18 -        in Syntax.const "_cabs" $ x $ t end
   22.19 +        in Syntax.const @{syntax_const "_cabs"} $ x $ t end
   22.20  
   22.21        | cabs_tr' _ T [t] = let
   22.22            val xT = domain_type (domain_type T);
   22.23            val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
   22.24            val (x,t') = atomic_abs_tr' abs';
   22.25 -        in Syntax.const "_cabs" $ x $ t' end;
   22.26 +        in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
   22.27  
   22.28    in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
   22.29  *}
   22.30 @@ -69,26 +69,28 @@
   22.31    "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
   22.32  
   22.33  parse_ast_translation {*
   22.34 -(* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
   22.35 -(* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
   22.36 +(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
   22.37 +(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
   22.38    let
   22.39      fun Lambda_ast_tr [pats, body] =
   22.40 -          Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body)
   22.41 +          Syntax.fold_ast_p @{syntax_const "_cabs"}
   22.42 +            (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
   22.43        | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
   22.44 -  in [("_Lambda", Lambda_ast_tr)] end;
   22.45 +  in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
   22.46  *}
   22.47  
   22.48  print_ast_translation {*
   22.49 -(* rewrites (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
   22.50 -(* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
   22.51 +(* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
   22.52 +(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
   22.53    let
   22.54      fun cabs_ast_tr' asts =
   22.55 -      (case Syntax.unfold_ast_p "_cabs"
   22.56 -          (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
   22.57 +      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
   22.58 +          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
   22.59          ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
   22.60        | (xs, body) => Syntax.Appl
   22.61 -          [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]);
   22.62 -  in [("_cabs", cabs_ast_tr')] end;
   22.63 +          [Syntax.Constant @{syntax_const "_Lambda"},
   22.64 +           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
   22.65 +  in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
   22.66  *}
   22.67  
   22.68  text {* Dummy patterns for continuous abstraction *}
    23.1 --- a/src/HOLCF/Fixrec.thy	Thu Feb 11 22:55:16 2010 +0100
    23.2 +++ b/src/HOLCF/Fixrec.thy	Thu Feb 11 23:00:22 2010 +0100
    23.3 @@ -226,10 +226,10 @@
    23.4    "_variable _noargs r" => "CONST unit_when\<cdot>r"
    23.5  
    23.6  parse_translation {*
    23.7 -(* rewrites (_pat x) => (return) *)
    23.8 -(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
    23.9 -  [("_pat", K (Syntax.const "Fixrec.return")),
   23.10 -   mk_binder_tr ("_variable", "Abs_CFun")];
   23.11 +(* rewrite (_pat x) => (return) *)
   23.12 +(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
   23.13 + [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.return}),
   23.14 +  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
   23.15  *}
   23.16  
   23.17  text {* Printing Case expressions *}
   23.18 @@ -240,23 +240,26 @@
   23.19  print_translation {*
   23.20    let
   23.21      fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
   23.22 -          (Syntax.const "_noargs", t)
   23.23 +          (Syntax.const @{syntax_const "_noargs"}, t)
   23.24      |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
   23.25            let
   23.26              val (v1, t1) = dest_LAM t;
   23.27              val (v2, t2) = dest_LAM t1;
   23.28 -          in (Syntax.const "_args" $ v1 $ v2, t2) end 
   23.29 +          in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
   23.30      |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
   23.31            let
   23.32 -            val abs = case t of Abs abs => abs
   23.33 +            val abs =
   23.34 +              case t of Abs abs => abs
   23.35                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   23.36              val (x, t') = atomic_abs_tr' abs;
   23.37 -          in (Syntax.const "_variable" $ x, t') end
   23.38 +          in (Syntax.const @{syntax_const "_variable"} $ x, t') end
   23.39      |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   23.40  
   23.41      fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
   23.42 -          let val (v, t) = dest_LAM r;
   23.43 -          in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
   23.44 +          let val (v, t) = dest_LAM r in
   23.45 +            Syntax.const @{syntax_const "_Case1"} $
   23.46 +              (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
   23.47 +          end;
   23.48  
   23.49    in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   23.50  *}
    24.1 --- a/src/HOLCF/Sprod.thy	Thu Feb 11 22:55:16 2010 +0100
    24.2 +++ b/src/HOLCF/Sprod.thy	Thu Feb 11 23:00:22 2010 +0100
    24.3 @@ -51,7 +51,7 @@
    24.4    "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    24.5  
    24.6  syntax
    24.7 -  "@stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
    24.8 +  "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
    24.9  translations
   24.10    "(:x, y, z:)" == "(:x, (:y, z:):)"
   24.11    "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"