modernized translations;
authorwenzelm
Thu Feb 11 22:19:58 2010 +0100 (2010-02-11)
changeset 351131a0c129bb2e0
parent 35112 ff6f60e6ab85
child 35114 b1fd1d756e20
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
doc-src/Classes/Thy/Setup.thy
src/CCL/Set.thy
src/CCL/Term.thy
src/CCL/Type.thy
src/Cube/Cube.thy
src/FOLP/IFOLP.thy
src/HOL/Hoare/HeapSyntax.thy
src/HOL/Hoare/HeapSyntaxAbort.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/Separation.thy
src/HOL/Hoare_Parallel/OG_Syntax.thy
src/HOL/Hoare_Parallel/Quote_Antiquote.thy
src/HOL/Hoare_Parallel/RG_Syntax.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/ex/Antiquote.thy
src/HOL/ex/Binary.thy
src/HOL/ex/Multiquote.thy
src/HOL/ex/Numeral.thy
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/Modal0.thy
src/Sequents/S43.thy
src/Sequents/Sequents.thy
     1.1 --- a/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 22:06:37 2010 +0100
     1.2 +++ b/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 22:19:58 2010 +0100
     1.3 @@ -18,17 +18,19 @@
     1.4      fun alpha_ast_tr [] = Syntax.Variable "'a"
     1.5        | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
     1.6      fun alpha_ofsort_ast_tr [ast] =
     1.7 -      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
     1.8 +      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
     1.9        | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    1.10      fun beta_ast_tr [] = Syntax.Variable "'b"
    1.11        | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.12      fun beta_ofsort_ast_tr [ast] =
    1.13 -      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
    1.14 +      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
    1.15        | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.16 -  in [
    1.17 -    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
    1.18 -    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
    1.19 -  ] end
    1.20 +  in
    1.21 +   [(@{syntax_const "_alpha"}, alpha_ast_tr),
    1.22 +    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
    1.23 +    (@{syntax_const "_beta"}, beta_ast_tr),
    1.24 +    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
    1.25 +  end
    1.26  *}
    1.27  
    1.28  end
    1.29 \ No newline at end of file
     2.1 --- a/src/CCL/Set.thy	Thu Feb 11 22:06:37 2010 +0100
     2.2 +++ b/src/CCL/Set.thy	Thu Feb 11 22:19:58 2010 +0100
     2.3 @@ -27,17 +27,17 @@
     2.4    empty         :: "'a set"                             ("{}")
     2.5  
     2.6  syntax
     2.7 -  "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
     2.8 +  "_Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
     2.9  
    2.10    (* Big Intersection / Union *)
    2.11  
    2.12 -  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    2.13 -  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    2.14 +  "_INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    2.15 +  "_UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    2.16  
    2.17    (* Bounded Quantifiers *)
    2.18  
    2.19 -  "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    2.20 -  "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    2.21 +  "_Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    2.22 +  "_Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    2.23  
    2.24  translations
    2.25    "{x. P}"      == "CONST Collect(%x. P)"
     3.1 --- a/src/CCL/Term.thy	Thu Feb 11 22:06:37 2010 +0100
     3.2 +++ b/src/CCL/Term.thy	Thu Feb 11 22:19:58 2010 +0100
     3.3 @@ -40,16 +40,16 @@
     3.4    letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
     3.5  
     3.6  syntax
     3.7 -  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
     3.8 +  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
     3.9                          [0,0,60] 60)
    3.10  
    3.11 -  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    3.12 +  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    3.13                          [0,0,0,60] 60)
    3.14  
    3.15 -  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    3.16 +  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    3.17                          [0,0,0,0,60] 60)
    3.18  
    3.19 -  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    3.20 +  "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    3.21                          [0,0,0,0,0,60] 60)
    3.22  
    3.23  ML {*
    3.24 @@ -58,29 +58,30 @@
    3.25  (* FIXME does not handle "_idtdummy" *)
    3.26  (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
    3.27  
    3.28 -fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
    3.29 +fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
    3.30  fun let_tr' [a,Abs(id,T,b)] =
    3.31       let val (id',b') = variant_abs(id,T,b)
    3.32 -     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
    3.33 +     in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
    3.34  
    3.35  fun letrec_tr [Free(f,S),Free(x,T),a,b] =
    3.36 -      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
    3.37 +      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
    3.38  fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
    3.39 -      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
    3.40 +      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
    3.41  fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
    3.42 -      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
    3.43 +      Const(@{const_syntax letrec3},dummyT) $
    3.44 +        absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
    3.45  
    3.46  fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
    3.47       let val (f',b')  = variant_abs(ff,SS,b)
    3.48           val (_,a'') = variant_abs(f,S,a)
    3.49           val (x',a')  = variant_abs(x,T,a'')
    3.50 -     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
    3.51 +     in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
    3.52  fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
    3.53       let val (f',b') = variant_abs(ff,SS,b)
    3.54           val ( _,a1) = variant_abs(f,S,a)
    3.55           val (y',a2) = variant_abs(y,U,a1)
    3.56           val (x',a') = variant_abs(x,T,a2)
    3.57 -     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
    3.58 +     in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
    3.59        end;
    3.60  fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
    3.61       let val (f',b') = variant_abs(ff,SS,b)
    3.62 @@ -88,22 +89,24 @@
    3.63           val (z',a2) = variant_abs(z,V,a1)
    3.64           val (y',a3) = variant_abs(y,U,a2)
    3.65           val (x',a') = variant_abs(x,T,a3)
    3.66 -     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
    3.67 +     in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
    3.68        end;
    3.69  
    3.70  *}
    3.71  
    3.72  parse_translation {*
    3.73 -  [("@let",       let_tr),
    3.74 -   ("@letrec",    letrec_tr),
    3.75 -   ("@letrec2",   letrec2_tr),
    3.76 -   ("@letrec3",   letrec3_tr)] *}
    3.77 + [(@{syntax_const "_let"}, let_tr),
    3.78 +  (@{syntax_const "_letrec"}, letrec_tr),
    3.79 +  (@{syntax_const "_letrec2"}, letrec2_tr),
    3.80 +  (@{syntax_const "_letrec3"}, letrec3_tr)]
    3.81 +*}
    3.82  
    3.83  print_translation {*
    3.84 -  [("let",       let_tr'),
    3.85 -   ("letrec",    letrec_tr'),
    3.86 -   ("letrec2",   letrec2_tr'),
    3.87 -   ("letrec3",   letrec3_tr')] *}
    3.88 + [(@{const_syntax let}, let_tr'),
    3.89 +  (@{const_syntax letrec}, letrec_tr'),
    3.90 +  (@{const_syntax letrec2}, letrec2_tr'),
    3.91 +  (@{const_syntax letrec3}, letrec3_tr')]
    3.92 +*}
    3.93  
    3.94  consts
    3.95    napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
     4.1 --- a/src/CCL/Type.thy	Thu Feb 11 22:06:37 2010 +0100
     4.2 +++ b/src/CCL/Type.thy	Thu Feb 11 22:19:58 2010 +0100
     4.3 @@ -28,15 +28,15 @@
     4.4    SPLIT         :: "[i, [i, i] => i set] => i set"
     4.5  
     4.6  syntax
     4.7 -  "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
     4.8 +  "_Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
     4.9                                  [0,0,60] 60)
    4.10  
    4.11 -  "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
    4.12 +  "_Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
    4.13                                  [0,0,60] 60)
    4.14  
    4.15 -  "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
    4.16 -  "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
    4.17 -  "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
    4.18 +  "_arrow"      :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
    4.19 +  "_star"       :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
    4.20 +  "_Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
    4.21  
    4.22  translations
    4.23    "PROD x:A. B" => "CONST Pi(A, %x. B)"
    4.24 @@ -46,8 +46,9 @@
    4.25    "{x: A. B}"   == "CONST Subtype(A, %x. B)"
    4.26  
    4.27  print_translation {*
    4.28 -  [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
    4.29 -   (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
    4.30 + [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
    4.31 +  (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
    4.32 +*}
    4.33  
    4.34  axioms
    4.35    Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
     5.1 --- a/src/Cube/Cube.thy	Thu Feb 11 22:06:37 2010 +0100
     5.2 +++ b/src/Cube/Cube.thy	Thu Feb 11 22:19:58 2010 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      Cube/Cube.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7  *)
     5.8  
     5.9 @@ -54,7 +53,9 @@
    5.10    Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
    5.11    arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
    5.12  
    5.13 -print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
    5.14 +print_translation {*
    5.15 +  [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))]
    5.16 +*}
    5.17  
    5.18  axioms
    5.19    s_b:          "*: []"
     6.1 --- a/src/FOLP/IFOLP.thy	Thu Feb 11 22:06:37 2010 +0100
     6.2 +++ b/src/FOLP/IFOLP.thy	Thu Feb 11 22:19:58 2010 +0100
     6.3 @@ -22,7 +22,6 @@
     6.4  
     6.5  consts
     6.6        (*** Judgements ***)
     6.7 - "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
     6.8   Proof          ::   "[o,p]=>prop"
     6.9   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    6.10  
    6.11 @@ -66,6 +65,8 @@
    6.12  
    6.13  local
    6.14  
    6.15 +syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
    6.16 +
    6.17  ML {*
    6.18  
    6.19  (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    6.20 @@ -74,12 +75,12 @@
    6.21  fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
    6.22  
    6.23  fun proof_tr' [P,p] =
    6.24 -    if !show_proofs then Const("@Proof",dummyT) $ p $ P
    6.25 -    else P  (*this case discards the proof term*);
    6.26 +  if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
    6.27 +  else P  (*this case discards the proof term*);
    6.28  *}
    6.29  
    6.30 -parse_translation {* [("@Proof", proof_tr)] *}
    6.31 -print_translation {* [("Proof", proof_tr')] *}
    6.32 +parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
    6.33 +print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
    6.34  
    6.35  axioms
    6.36  
     7.1 --- a/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:06:37 2010 +0100
     7.2 +++ b/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:19:58 2010 +0100
     7.3 @@ -15,9 +15,9 @@
     7.4    "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
     7.5     ("_^._" [65,1000] 65)
     7.6  translations
     7.7 -  "f(r \<rightarrow> v)"  ==  "f(CONST addr r := v)"
     7.8 -  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
     7.9 -  "p^.f"       =>  "f(CONST addr p)"
    7.10 +  "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
    7.11 +  "p^.f := e" => "f := f(p \<rightarrow> e)"
    7.12 +  "p^.f" => "f(CONST addr p)"
    7.13  
    7.14  
    7.15  declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
     8.1 --- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 22:06:37 2010 +0100
     8.2 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 22:19:58 2010 +0100
     8.3 @@ -23,9 +23,9 @@
     8.4    "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
     8.5     ("_^._" [65,1000] 65)
     8.6  translations
     8.7 -  "_refupdate f r v"  ==  "f(CONST addr r := v)"
     8.8 -  "p^.f := e"  =>  "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
     8.9 -  "p^.f"       =>  "f(CONST addr p)"
    8.10 +  "_refupdate f r v" == "f(CONST addr r := v)"
    8.11 +  "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
    8.12 +  "p^.f" => "f(CONST addr p)"
    8.13  
    8.14  
    8.15  declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
     9.1 --- a/src/HOL/Hoare/Hoare.thy	Thu Feb 11 22:06:37 2010 +0100
     9.2 +++ b/src/HOL/Hoare/Hoare.thy	Thu Feb 11 22:19:58 2010 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Hoare/Hoare.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Leonor Prensa Nieto & Tobias Nipkow
     9.7      Copyright   1998 TUM
     9.8  
     9.9 @@ -19,11 +18,11 @@
    9.10      'a assn = "'a set"
    9.11  
    9.12  datatype
    9.13 - 'a com = Basic "'a \<Rightarrow> 'a"         
    9.14 + 'a com = Basic "'a \<Rightarrow> 'a"
    9.15     | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    9.16     | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    9.17     | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    9.18 -  
    9.19 +
    9.20  abbreviation annskip ("SKIP") where "SKIP == Basic id"
    9.21  
    9.22  types 'a sem = "'a => 'a => bool"
    9.23 @@ -68,11 +67,11 @@
    9.24  
    9.25  fun mk_abstuple [x] body = abs (x, body)
    9.26    | mk_abstuple (x::xs) body =
    9.27 -      Syntax.const "split" $ abs (x, mk_abstuple xs body);
    9.28 +      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
    9.29  
    9.30  fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
    9.31    | mk_fbody a e ((b,_)::xs) =
    9.32 -      Syntax.const "Pair" $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
    9.33 +      Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
    9.34  
    9.35  fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
    9.36  end
    9.37 @@ -82,22 +81,22 @@
    9.38  (*all meta-variables for bexp except for TRUE are translated as if they
    9.39    were boolean expressions*)
    9.40  ML{*
    9.41 -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
    9.42 -  | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
    9.43 -  
    9.44 -fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
    9.45 +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
    9.46 +  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
    9.47 +
    9.48 +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
    9.49  *}
    9.50  (* com_tr *)
    9.51  ML{*
    9.52 -fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
    9.53 -      Syntax.const "Basic" $ mk_fexp a e xs
    9.54 -  | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
    9.55 -  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
    9.56 -      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
    9.57 -  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
    9.58 -      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
    9.59 -  | com_tr (Const ("While",_) $ b $ I $ c) xs =
    9.60 -      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
    9.61 +fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
    9.62 +      Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
    9.63 +  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
    9.64 +  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
    9.65 +      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
    9.66 +  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
    9.67 +      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
    9.68 +  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
    9.69 +      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
    9.70    | com_tr t _ = t (* if t is just a Free/Var *)
    9.71  *}
    9.72  
    9.73 @@ -106,65 +105,66 @@
    9.74  local
    9.75  
    9.76  fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
    9.77 -  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
    9.78 +  | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T);
    9.79  
    9.80 -fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
    9.81 +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
    9.82    | vars_tr t = [var_tr t]
    9.83  
    9.84  in
    9.85  fun hoare_vars_tr [vars, pre, prg, post] =
    9.86        let val xs = vars_tr vars
    9.87 -      in Syntax.const "Valid" $
    9.88 +      in Syntax.const @{const_syntax Valid} $
    9.89           assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
    9.90        end
    9.91    | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
    9.92  end
    9.93  *}
    9.94  
    9.95 -parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
    9.96 +parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
    9.97  
    9.98  
    9.99  (*****************************************************************************)
   9.100  
   9.101  (*** print translations ***)
   9.102  ML{*
   9.103 -fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
   9.104 +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
   9.105                              subst_bound (Syntax.free v, dest_abstuple body)
   9.106    | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   9.107    | dest_abstuple trm = trm;
   9.108  
   9.109 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   9.110 +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   9.111    | abs2list (Abs(x,T,t)) = [Free (x, T)]
   9.112    | abs2list _ = [];
   9.113  
   9.114 -fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
   9.115 +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
   9.116    | mk_ts (Abs(x,_,t)) = mk_ts t
   9.117 -  | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
   9.118 +  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   9.119    | mk_ts t = [t];
   9.120  
   9.121 -fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = 
   9.122 +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
   9.123             ((Syntax.free x)::(abs2list t), mk_ts t)
   9.124    | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   9.125    | mk_vts t = raise Match;
   9.126 -  
   9.127 -fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
   9.128 -  | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
   9.129 -              else (true, (v, subst_bounds (xs,t)));
   9.130 -  
   9.131 -fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
   9.132 +
   9.133 +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
   9.134 +  | find_ch ((v,t)::vts) i xs =
   9.135 +      if t = Bound i then find_ch vts (i-1) xs
   9.136 +      else (true, (v, subst_bounds (xs, t)));
   9.137 +
   9.138 +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
   9.139    | is_f (Abs(x,_,t)) = true
   9.140    | is_f t = false;
   9.141  *}
   9.142  
   9.143  (* assn_tr' & bexp_tr'*)
   9.144 -ML{*  
   9.145 -fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
   9.146 -  | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $ 
   9.147 -                                   (Const ("Collect",_) $ T2)) =  
   9.148 -            Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
   9.149 +ML{*
   9.150 +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
   9.151 +  | assn_tr' (Const (@{const_syntax inter}, _) $
   9.152 +        (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
   9.153 +      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
   9.154    | assn_tr' t = t;
   9.155  
   9.156 -fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
   9.157 +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
   9.158    | bexp_tr' t = t;
   9.159  *}
   9.160  
   9.161 @@ -173,22 +173,24 @@
   9.162  fun mk_assign f =
   9.163    let val (vs, ts) = mk_vts f;
   9.164        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
   9.165 -  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
   9.166 -     else Syntax.const @{const_syntax annskip} end;
   9.167 +  in
   9.168 +    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
   9.169 +    else Syntax.const @{const_syntax annskip}
   9.170 +  end;
   9.171  
   9.172 -fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
   9.173 -                                           else Syntax.const "Basic" $ f
   9.174 -  | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
   9.175 -                                                 com_tr' c1 $ com_tr' c2
   9.176 -  | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
   9.177 -                                           bexp_tr' b $ com_tr' c1 $ com_tr' c2
   9.178 -  | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
   9.179 -                                               bexp_tr' b $ assn_tr' I $ com_tr' c
   9.180 +fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
   9.181 +      if is_f f then mk_assign f
   9.182 +      else Syntax.const @{const_syntax Basic} $ f
   9.183 +  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
   9.184 +      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
   9.185 +  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
   9.186 +      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
   9.187 +  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
   9.188 +      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
   9.189    | com_tr' t = t;
   9.190  
   9.191 -
   9.192  fun spec_tr' [p, c, q] =
   9.193 -  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
   9.194 +  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
   9.195  *}
   9.196  
   9.197  print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
    10.1 --- a/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 22:06:37 2010 +0100
    10.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 22:19:58 2010 +0100
    10.3 @@ -20,7 +20,7 @@
    10.4     | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    10.5     | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    10.6     | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
    10.7 -  
    10.8 +
    10.9  abbreviation annskip ("SKIP") where "SKIP == Basic id"
   10.10  
   10.11  types 'a sem = "'a option => 'a option => bool"
   10.12 @@ -69,11 +69,11 @@
   10.13  
   10.14  fun mk_abstuple [x] body = abs (x, body)
   10.15    | mk_abstuple (x::xs) body =
   10.16 -      Syntax.const "split" $ abs (x, mk_abstuple xs body);
   10.17 +      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
   10.18  
   10.19  fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
   10.20    | mk_fbody a e ((b,_)::xs) =
   10.21 -      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
   10.22 +      Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
   10.23  
   10.24  fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
   10.25  end
   10.26 @@ -83,22 +83,22 @@
   10.27  (*all meta-variables for bexp except for TRUE are translated as if they
   10.28    were boolean expressions*)
   10.29  ML{*
   10.30 -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
   10.31 -  | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
   10.32 -  
   10.33 -fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
   10.34 +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
   10.35 +  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
   10.36 +
   10.37 +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
   10.38  *}
   10.39  (* com_tr *)
   10.40  ML{*
   10.41 -fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
   10.42 -      Syntax.const "Basic" $ mk_fexp a e xs
   10.43 -  | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
   10.44 -  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
   10.45 -      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
   10.46 -  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
   10.47 -      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
   10.48 -  | com_tr (Const ("While",_) $ b $ I $ c) xs =
   10.49 -      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   10.50 +fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
   10.51 +      Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
   10.52 +  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
   10.53 +  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
   10.54 +      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
   10.55 +  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
   10.56 +      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
   10.57 +  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
   10.58 +      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   10.59    | com_tr t _ = t (* if t is just a Free/Var *)
   10.60  *}
   10.61  
   10.62 @@ -106,66 +106,67 @@
   10.63  ML{*
   10.64  local
   10.65  
   10.66 -fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
   10.67 -  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
   10.68 +fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
   10.69 +  | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
   10.70  
   10.71 -fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
   10.72 +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
   10.73    | vars_tr t = [var_tr t]
   10.74  
   10.75  in
   10.76  fun hoare_vars_tr [vars, pre, prg, post] =
   10.77        let val xs = vars_tr vars
   10.78 -      in Syntax.const "Valid" $
   10.79 +      in Syntax.const @{const_syntax Valid} $
   10.80           assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
   10.81        end
   10.82    | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
   10.83  end
   10.84  *}
   10.85  
   10.86 -parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
   10.87 +parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
   10.88  
   10.89  
   10.90  (*****************************************************************************)
   10.91  
   10.92  (*** print translations ***)
   10.93  ML{*
   10.94 -fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
   10.95 -                            subst_bound (Syntax.free v, dest_abstuple body)
   10.96 +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
   10.97 +      subst_bound (Syntax.free v, dest_abstuple body)
   10.98    | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   10.99    | dest_abstuple trm = trm;
  10.100  
  10.101 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
  10.102 +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
  10.103    | abs2list (Abs(x,T,t)) = [Free (x, T)]
  10.104    | abs2list _ = [];
  10.105  
  10.106 -fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
  10.107 +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
  10.108    | mk_ts (Abs(x,_,t)) = mk_ts t
  10.109 -  | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
  10.110 +  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
  10.111    | mk_ts t = [t];
  10.112  
  10.113 -fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = 
  10.114 +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
  10.115             ((Syntax.free x)::(abs2list t), mk_ts t)
  10.116    | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
  10.117    | mk_vts t = raise Match;
  10.118 -  
  10.119 -fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
  10.120 -  | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
  10.121 -              else (true, (v, subst_bounds (xs,t)));
  10.122 -  
  10.123 -fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
  10.124 +
  10.125 +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
  10.126 +  | find_ch ((v,t)::vts) i xs =
  10.127 +      if t = Bound i then find_ch vts (i-1) xs
  10.128 +      else (true, (v, subst_bounds (xs,t)));
  10.129 +
  10.130 +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
  10.131    | is_f (Abs(x,_,t)) = true
  10.132    | is_f t = false;
  10.133  *}
  10.134  
  10.135  (* assn_tr' & bexp_tr'*)
  10.136 -ML{*  
  10.137 -fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
  10.138 -  | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $ 
  10.139 -                                   (Const ("Collect",_) $ T2)) =  
  10.140 -            Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
  10.141 +ML{*
  10.142 +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
  10.143 +  | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
  10.144 +        (Const (@{const_syntax Collect},_) $ T2)) =
  10.145 +      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
  10.146    | assn_tr' t = t;
  10.147  
  10.148 -fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
  10.149 +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
  10.150    | bexp_tr' t = t;
  10.151  *}
  10.152  
  10.153 @@ -174,22 +175,23 @@
  10.154  fun mk_assign f =
  10.155    let val (vs, ts) = mk_vts f;
  10.156        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
  10.157 -  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
  10.158 -     else Syntax.const @{const_syntax annskip} end;
  10.159 +  in
  10.160 +    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
  10.161 +    else Syntax.const @{const_syntax annskip}
  10.162 +  end;
  10.163  
  10.164 -fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
  10.165 -                                           else Syntax.const "Basic" $ f
  10.166 -  | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
  10.167 -                                                 com_tr' c1 $ com_tr' c2
  10.168 -  | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
  10.169 -                                           bexp_tr' b $ com_tr' c1 $ com_tr' c2
  10.170 -  | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
  10.171 -                                               bexp_tr' b $ assn_tr' I $ com_tr' c
  10.172 +fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
  10.173 +      if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
  10.174 +  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
  10.175 +      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
  10.176 +  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
  10.177 +      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
  10.178 +  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
  10.179 +      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
  10.180    | com_tr' t = t;
  10.181  
  10.182 -
  10.183  fun spec_tr' [p, c, q] =
  10.184 -  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
  10.185 +  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
  10.186  *}
  10.187  
  10.188  print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
    11.1 --- a/src/HOL/Hoare/Separation.thy	Thu Feb 11 22:06:37 2010 +0100
    11.2 +++ b/src/HOL/Hoare/Separation.thy	Thu Feb 11 22:19:58 2010 +0100
    11.3 @@ -64,22 +64,25 @@
    11.4  *)
    11.5    | free_tr t = t
    11.6  
    11.7 -fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
    11.8 +fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
    11.9    | emp_tr ts = raise TERM ("emp_tr", ts);
   11.10 -fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
   11.11 +fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
   11.12    | singl_tr ts = raise TERM ("singl_tr", ts);
   11.13 -fun star_tr [P,Q] = Syntax.const "star" $
   11.14 -      absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
   11.15 +fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
   11.16 +      absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
   11.17        Syntax.free "H"
   11.18    | star_tr ts = raise TERM ("star_tr", ts);
   11.19 -fun wand_tr [P,Q] = Syntax.const "wand" $
   11.20 -      absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
   11.21 +fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
   11.22 +      absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
   11.23    | wand_tr ts = raise TERM ("wand_tr", ts);
   11.24  *}
   11.25  
   11.26 -parse_translation
   11.27 - {* [("_emp", emp_tr), ("_singl", singl_tr),
   11.28 -     ("_star", star_tr), ("_wand", wand_tr)] *}
   11.29 +parse_translation {*
   11.30 + [(@{syntax_const "_emp"}, emp_tr),
   11.31 +  (@{syntax_const "_singl"}, singl_tr),
   11.32 +  (@{syntax_const "_star"}, star_tr),
   11.33 +  (@{syntax_const "_wand"}, wand_tr)]
   11.34 +*}
   11.35  
   11.36  text{* Now it looks much better: *}
   11.37  
   11.38 @@ -102,17 +105,9 @@
   11.39  text{* But the output is still unreadable. Thus we also strip the heap
   11.40  parameters upon output: *}
   11.41  
   11.42 -(* debugging code:
   11.43 -fun sot(Free(s,_)) = s
   11.44 -  | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i
   11.45 -  | sot(Const(s,_)) = s
   11.46 -  | sot(Bound i) = "B." ^ string_of_int i
   11.47 -  | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")"
   11.48 -  | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")";
   11.49 -*)
   11.50 +ML {*
   11.51 +local
   11.52  
   11.53 -ML{*
   11.54 -local
   11.55  fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
   11.56    | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
   11.57  (*
   11.58 @@ -120,19 +115,25 @@
   11.59  *)
   11.60    | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   11.61    | strip (Abs(_,_,P)) = P
   11.62 -  | strip (Const("is_empty",_)) = Syntax.const "_emp"
   11.63 +  | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
   11.64    | strip t = t;
   11.65 +
   11.66  in
   11.67 -fun is_empty_tr' [_] = Syntax.const "_emp"
   11.68 -fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
   11.69 -fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
   11.70 -fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
   11.71 +
   11.72 +fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
   11.73 +fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} $ p $ q
   11.74 +fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} $ strip P $ strip Q
   11.75 +fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} $ strip P $ strip Q
   11.76 +
   11.77  end
   11.78  *}
   11.79  
   11.80 -print_translation
   11.81 - {* [("is_empty", is_empty_tr'),("singl", singl_tr'),
   11.82 -     ("star", star_tr'),("wand", wand_tr')] *}
   11.83 +print_translation {*
   11.84 + [(@{const_syntax is_empty}, is_empty_tr'),
   11.85 +  (@{const_syntax singl}, singl_tr'),
   11.86 +  (@{const_syntax star}, star_tr'),
   11.87 +  (@{const_syntax wand}, wand_tr')]
   11.88 +*}
   11.89  
   11.90  text{* Now the intermediate proof states are also readable: *}
   11.91  
    12.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 22:06:37 2010 +0100
    12.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 22:19:58 2010 +0100
    12.3 @@ -46,14 +46,14 @@
    12.4  translations
    12.5    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
    12.6    "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    12.7 -  "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
    12.8 +  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While .{b}. i c"
    12.9    "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
   12.10  
   12.11    "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2"
   12.12    "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c"
   12.13    "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c"
   12.14    "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c"
   12.15 -  "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END"
   12.16 +  "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
   12.17    "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
   12.18   
   12.19  nonterminals
   12.20 @@ -77,14 +77,14 @@
   12.21  print_translation {*
   12.22    let
   12.23      fun quote_tr' f (t :: ts) =
   12.24 -          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
   12.25 +          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   12.26        | quote_tr' _ _ = raise Match;
   12.27  
   12.28      fun annquote_tr' f (r :: t :: ts) =
   12.29 -          Term.list_comb (f $ r $ Syntax.quote_tr' "_antiquote" t, ts)
   12.30 +          Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   12.31        | annquote_tr' _ _ = raise Match;
   12.32  
   12.33 -    val assert_tr' = quote_tr' (Syntax.const "_Assert");
   12.34 +    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   12.35  
   12.36      fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
   12.37            quote_tr' (Syntax.const name) (t :: ts)
   12.38 @@ -100,7 +100,7 @@
   12.39        | NONE => raise Match);
   12.40  
   12.41      fun update_name_tr' (Free x) = Free (upd_tr' x)
   12.42 -      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
   12.43 +      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
   12.44            c $ Free (upd_tr' x)
   12.45        | update_name_tr' (Const x) = Const (upd_tr' x)
   12.46        | update_name_tr' _ = raise Match;
   12.47 @@ -112,24 +112,24 @@
   12.48        | K_tr' _ = raise Match;
   12.49  
   12.50      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   12.51 -          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
   12.52 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
   12.53              (Abs (x, dummyT, K_tr' k) :: ts)
   12.54        | assign_tr' _ = raise Match;
   12.55  
   12.56      fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
   12.57 -          quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
   12.58 +          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ update_name_tr' f)
   12.59              (Abs (x, dummyT, K_tr' k) :: ts)
   12.60        | annassign_tr' _ = raise Match;
   12.61  
   12.62      fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
   12.63              (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $
   12.64 -            Const (@{const_syntax Nil}, _))] = Syntax.const "_prg" $ t1 $ t2
   12.65 +            Const (@{const_syntax Nil}, _))] = Syntax.const @{syntax_const "_prg"} $ t1 $ t2
   12.66        | Parallel_PAR [(Const (@{const_syntax Cons}, _) $
   12.67              (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] =
   12.68 -          Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts]
   12.69 +          Syntax.const @{syntax_const "_prgs"} $ t1 $ t2 $ Parallel_PAR [ts]
   12.70        | Parallel_PAR _ = raise Match;
   12.71  
   12.72 -    fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts;
   12.73 +    fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
   12.74    in
   12.75     [(@{const_syntax Collect}, assert_tr'),
   12.76      (@{const_syntax Basic}, assign_tr'),
    13.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
    13.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:19:58 2010 +0100
    13.3 @@ -16,9 +16,9 @@
    13.4  
    13.5  parse_translation {*
    13.6    let
    13.7 -    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
    13.8 +    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
    13.9        | quote_tr ts = raise TERM ("quote_tr", ts);
   13.10 -  in [("_quote", quote_tr)] end
   13.11 +  in [(@{syntax_const "_quote"}, quote_tr)] end
   13.12  *}
   13.13  
   13.14  end
   13.15 \ No newline at end of file
    14.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 22:06:37 2010 +0100
    14.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 22:19:58 2010 +0100
    14.3 @@ -20,11 +20,11 @@
    14.4  
    14.5  translations
    14.6    "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
    14.7 -  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    14.8 +  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
    14.9    "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
   14.10 -  "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c"
   14.11 -  "AWAIT b THEN c END" \<rightleftharpoons> "Await .{b}. c"
   14.12 -  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT True THEN c END"
   14.13 +  "WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c"
   14.14 +  "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c"
   14.15 +  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
   14.16    "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
   14.17  
   14.18  nonterminals
   14.19 @@ -59,10 +59,10 @@
   14.20  print_translation {*
   14.21    let
   14.22      fun quote_tr' f (t :: ts) =
   14.23 -          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
   14.24 +          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   14.25        | quote_tr' _ _ = raise Match;
   14.26  
   14.27 -    val assert_tr' = quote_tr' (Syntax.const "_Assert");
   14.28 +    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   14.29  
   14.30      fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
   14.31            quote_tr' (Syntax.const name) (t :: ts)
   14.32 @@ -74,7 +74,7 @@
   14.33        | NONE => raise Match);
   14.34  
   14.35      fun update_name_tr' (Free x) = Free (upd_tr' x)
   14.36 -      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
   14.37 +      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
   14.38            c $ Free (upd_tr' x)
   14.39        | update_name_tr' (Const x) = Const (upd_tr' x)
   14.40        | update_name_tr' _ = raise Match;
   14.41 @@ -86,14 +86,14 @@
   14.42        | K_tr' _ = raise Match;
   14.43  
   14.44      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   14.45 -          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
   14.46 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
   14.47              (Abs (x, dummyT, K_tr' k) :: ts)
   14.48        | assign_tr' _ = raise Match;
   14.49    in
   14.50     [(@{const_syntax Collect}, assert_tr'),
   14.51      (@{const_syntax Basic}, assign_tr'),
   14.52 -    (@{const_syntax Cond}, bexp_tr' "_Cond"),
   14.53 -    (@{const_syntax While}, bexp_tr' "_While_inv")]
   14.54 +    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
   14.55 +    (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
   14.56    end
   14.57  *}
   14.58  
    15.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:06:37 2010 +0100
    15.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:19:58 2010 +0100
    15.3 @@ -147,16 +147,16 @@
    15.4            val v_used = fold_aterms
    15.5              (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
    15.6          in if v_used then
    15.7 -          Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
    15.8 +          Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g'
    15.9          else
   15.10 -          Const ("_chainM", dummyT) $ f $ unfold_monad g'
   15.11 +          Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g'
   15.12          end
   15.13      | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
   15.14 -        Const ("_chainM", dummyT) $ f $ unfold_monad g
   15.15 +        Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g
   15.16      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   15.17          let
   15.18            val (v, g') = dest_abs_eta g;
   15.19 -        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
   15.20 +        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
   15.21      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   15.22          Const (@{const_syntax return}, dummyT) $ f
   15.23      | unfold_monad f = f;
   15.24 @@ -164,14 +164,17 @@
   15.25      | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   15.26          contains_bindM t;
   15.27    fun bindM_monad_tr' (f::g::ts) = list_comb
   15.28 -    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
   15.29 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
   15.30 -      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   15.31 +    (Const (@{syntax_const "_do"}, dummyT) $
   15.32 +      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
   15.33 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   15.34 +    if contains_bindM g' then list_comb
   15.35 +      (Const (@{syntax_const "_do"}, dummyT) $
   15.36 +        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   15.37      else raise Match;
   15.38 -in [
   15.39 -  (@{const_syntax bindM}, bindM_monad_tr'),
   15.40 -  (@{const_syntax Let}, Let_monad_tr')
   15.41 -] end;
   15.42 +in
   15.43 + [(@{const_syntax bindM}, bindM_monad_tr'),
   15.44 +  (@{const_syntax Let}, Let_monad_tr')]
   15.45 +end;
   15.46  *}
   15.47  
   15.48  
    16.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 22:06:37 2010 +0100
    16.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 22:19:58 2010 +0100
    16.3 @@ -237,9 +237,9 @@
    16.4  
    16.5  parse_translation {*
    16.6    let
    16.7 -    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
    16.8 +    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
    16.9        | quote_tr ts = raise TERM ("quote_tr", ts);
   16.10 -  in [("_quote", quote_tr)] end
   16.11 +  in [(@{syntax_const "_quote"}, quote_tr)] end
   16.12  *}
   16.13  
   16.14  text {*
   16.15 @@ -251,12 +251,12 @@
   16.16  print_translation {*
   16.17    let
   16.18      fun quote_tr' f (t :: ts) =
   16.19 -          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
   16.20 +          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
   16.21        | quote_tr' _ _ = raise Match;
   16.22  
   16.23 -    val assert_tr' = quote_tr' (Syntax.const "_Assert");
   16.24 +    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   16.25  
   16.26 -    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
   16.27 +    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
   16.28            quote_tr' (Syntax.const name) (t :: ts)
   16.29        | bexp_tr' _ _ = raise Match;
   16.30  
   16.31 @@ -266,7 +266,7 @@
   16.32        | NONE => raise Match);
   16.33  
   16.34      fun update_name_tr' (Free x) = Free (upd_tr' x)
   16.35 -      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
   16.36 +      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
   16.37            c $ Free (upd_tr' x)
   16.38        | update_name_tr' (Const x) = Const (upd_tr' x)
   16.39        | update_name_tr' _ = raise Match;
   16.40 @@ -276,12 +276,14 @@
   16.41        | K_tr' _ = raise Match;
   16.42  
   16.43      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   16.44 -          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
   16.45 +          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
   16.46              (Abs (x, dummyT, K_tr' k) :: ts)
   16.47        | assign_tr' _ = raise Match;
   16.48    in
   16.49 -    [("Collect", assert_tr'), ("Basic", assign_tr'),
   16.50 -      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
   16.51 +   [(@{const_syntax Collect}, assert_tr'),
   16.52 +    (@{const_syntax Basic}, assign_tr'),
   16.53 +    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
   16.54 +    (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
   16.55    end
   16.56  *}
   16.57  
    17.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 22:06:37 2010 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 22:19:58 2010 +0100
    17.3 @@ -27,14 +27,14 @@
    17.4  
    17.5  parse_translation {*
    17.6  let
    17.7 -  fun cart t u = Syntax.const @{type_name cart} $ t $ u
    17.8 +  fun cart t u = Syntax.const @{type_name cart} $ t $ u;   (* FIXME @{type_syntax} *)
    17.9    fun finite_cart_tr [t, u as Free (x, _)] =
   17.10 -        if Syntax.is_tid x
   17.11 -        then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite}))
   17.12 +        if Syntax.is_tid x then
   17.13 +          cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite}))
   17.14          else cart t u
   17.15      | finite_cart_tr [t, u] = cart t u
   17.16  in
   17.17 -  [("_finite_cart", finite_cart_tr)]
   17.18 +  [(@{syntax_const "_finite_cart"}, finite_cart_tr)]
   17.19  end
   17.20  *}
   17.21  
    18.1 --- a/src/HOL/ex/Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
    18.2 +++ b/src/HOL/ex/Antiquote.thy	Thu Feb 11 22:19:58 2010 +0100
    18.3 @@ -1,11 +1,12 @@
    18.4  (*  Title:      HOL/ex/Antiquote.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Markus Wenzel, TU Muenchen
    18.7  *)
    18.8  
    18.9  header {* Antiquotations *}
   18.10  
   18.11 -theory Antiquote imports Main begin
   18.12 +theory Antiquote
   18.13 +imports Main
   18.14 +begin
   18.15  
   18.16  text {*
   18.17    A simple example on quote / antiquote in higher-order abstract
   18.18 @@ -13,17 +14,23 @@
   18.19  *}
   18.20  
   18.21  syntax
   18.22 -  "_Expr" :: "'a => 'a"                         ("EXPR _" [1000] 999)
   18.23 +  "_Expr" :: "'a => 'a"    ("EXPR _" [1000] 999)
   18.24  
   18.25 -constdefs
   18.26 -  var :: "'a => ('a => nat) => nat"             ("VAR _" [1000] 999)
   18.27 -  "var x env == env x"
   18.28 +definition
   18.29 +  var :: "'a => ('a => nat) => nat"    ("VAR _" [1000] 999)
   18.30 +  where "var x env = env x"
   18.31  
   18.32 +definition
   18.33    Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
   18.34 -  "Expr exp env == exp env"
   18.35 +  where "Expr exp env = exp env"
   18.36  
   18.37 -parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
   18.38 -print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
   18.39 +parse_translation {*
   18.40 +  [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
   18.41 +*}
   18.42 +
   18.43 +print_translation {*
   18.44 +  [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
   18.45 +*}
   18.46  
   18.47  term "EXPR (a + b + c)"
   18.48  term "EXPR (a + b + c + VAR x + VAR y + 1)"
    19.1 --- a/src/HOL/ex/Binary.thy	Thu Feb 11 22:06:37 2010 +0100
    19.2 +++ b/src/HOL/ex/Binary.thy	Thu Feb 11 22:19:58 2010 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOL/ex/Binary.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Makarius
    19.7  *)
    19.8  
    19.9 @@ -21,8 +20,6 @@
   19.10    unfolding bit_def by simp_all
   19.11  
   19.12  ML {*
   19.13 -structure Binary =
   19.14 -struct
   19.15    fun dest_bit (Const (@{const_name False}, _)) = 0
   19.16      | dest_bit (Const (@{const_name True}, _)) = 1
   19.17      | dest_bit t = raise TERM ("dest_bit", [t]);
   19.18 @@ -43,7 +40,6 @@
   19.19          else
   19.20            let val (q, r) = Integer.div_mod n 2
   19.21            in @{term bit} $ mk_binary q $ mk_bit r end;
   19.22 -end
   19.23  *}
   19.24  
   19.25  
   19.26 @@ -126,7 +122,7 @@
   19.27    fun binary_proc proc ss ct =
   19.28      (case Thm.term_of ct of
   19.29        _ $ t $ u =>
   19.30 -      (case try (pairself (`Binary.dest_binary)) (t, u) of
   19.31 +      (case try (pairself (`dest_binary)) (t, u) of
   19.32          SOME args => proc (Simplifier.the_context ss) args
   19.33        | NONE => NONE)
   19.34      | _ => NONE);
   19.35 @@ -135,34 +131,34 @@
   19.36  val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   19.37    let val k = n - m in
   19.38      if k >= 0 then
   19.39 -      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
   19.40 +      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
   19.41      else
   19.42        SOME (@{thm binary_less_eq(2)} OF
   19.43 -        [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
   19.44 +        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
   19.45    end);
   19.46  
   19.47  val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   19.48    let val k = m - n in
   19.49      if k >= 0 then
   19.50 -      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
   19.51 +      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
   19.52      else
   19.53        SOME (@{thm binary_less(2)} OF
   19.54 -        [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
   19.55 +        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
   19.56    end);
   19.57  
   19.58  val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   19.59    let val k = m - n in
   19.60      if k >= 0 then
   19.61 -      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
   19.62 +      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
   19.63      else
   19.64 -      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
   19.65 +      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
   19.66    end);
   19.67  
   19.68  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   19.69    if n = 0 then NONE
   19.70    else
   19.71      let val (k, l) = Integer.div_mod m n
   19.72 -    in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
   19.73 +    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
   19.74  
   19.75  end;
   19.76  *}
   19.77 @@ -194,17 +190,17 @@
   19.78  
   19.79  parse_translation {*
   19.80  let
   19.81 -
   19.82 -val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
   19.83 +  val syntax_consts =
   19.84 +    map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
   19.85  
   19.86 -fun binary_tr [Const (num, _)] =
   19.87 -      let
   19.88 -        val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
   19.89 -        val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   19.90 -      in syntax_consts (Binary.mk_binary n) end
   19.91 -  | binary_tr ts = raise TERM ("binary_tr", ts);
   19.92 +  fun binary_tr [Const (num, _)] =
   19.93 +        let
   19.94 +          val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
   19.95 +          val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   19.96 +        in syntax_consts (mk_binary n) end
   19.97 +    | binary_tr ts = raise TERM ("binary_tr", ts);
   19.98  
   19.99 -in [("_Binary", binary_tr)] end
  19.100 +in [(@{syntax_const "_Binary"}, binary_tr)] end
  19.101  *}
  19.102  
  19.103  
    20.1 --- a/src/HOL/ex/Multiquote.thy	Thu Feb 11 22:06:37 2010 +0100
    20.2 +++ b/src/HOL/ex/Multiquote.thy	Thu Feb 11 22:19:58 2010 +0100
    20.3 @@ -1,11 +1,12 @@
    20.4  (*  Title:      HOL/ex/Multiquote.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Markus Wenzel, TU Muenchen
    20.7  *)
    20.8  
    20.9  header {* Multiple nested quotations and anti-quotations *}
   20.10  
   20.11 -theory Multiquote imports Main begin
   20.12 +theory Multiquote
   20.13 +imports Main
   20.14 +begin
   20.15  
   20.16  text {*
   20.17    Multiple nested quotations and anti-quotations -- basically a
   20.18 @@ -13,25 +14,25 @@
   20.19  *}
   20.20  
   20.21  syntax
   20.22 -  "_quote" :: "'b => ('a => 'b)"             ("\<guillemotleft>_\<guillemotright>" [0] 1000)
   20.23 -  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
   20.24 +  "_quote" :: "'b => ('a => 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
   20.25 +  "_antiquote" :: "('a => 'b) => 'b"    ("\<acute>_" [1000] 1000)
   20.26  
   20.27  parse_translation {*
   20.28    let
   20.29 -    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
   20.30 -          skip_antiquote_tr i t
   20.31 -      | antiquote_tr i (Const ("_antiquote", _) $ t) =
   20.32 +    fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
   20.33 +          (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
   20.34 +      | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
   20.35            antiquote_tr i t $ Bound i
   20.36        | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
   20.37        | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
   20.38        | antiquote_tr _ a = a
   20.39 -    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
   20.40 +    and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
   20.41            c $ skip_antiquote_tr i t
   20.42        | skip_antiquote_tr i t = antiquote_tr i t;
   20.43  
   20.44      fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
   20.45        | quote_tr ts = raise TERM ("quote_tr", ts);
   20.46 -  in [("_quote", quote_tr)] end
   20.47 +  in [(@{syntax_const "_quote"}, quote_tr)] end
   20.48  *}
   20.49  
   20.50  text {* basic examples *}
    21.1 --- a/src/HOL/ex/Numeral.thy	Thu Feb 11 22:06:37 2010 +0100
    21.2 +++ b/src/HOL/ex/Numeral.thy	Thu Feb 11 22:19:58 2010 +0100
    21.3 @@ -311,7 +311,7 @@
    21.4              orelse error ("Bad numeral: " ^ num);
    21.5          in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
    21.6      | numeral_tr ts = raise TERM ("numeral_tr", ts);
    21.7 -in [("_Numerals", numeral_tr)] end
    21.8 +in [(@{syntax_const "_Numerals"}, numeral_tr)] end
    21.9  *}
   21.10  
   21.11  typed_print_translation {*
   21.12 @@ -325,9 +325,9 @@
   21.13    fun num_tr' show_sorts T [n] =
   21.14      let
   21.15        val k = int_of_num' n;
   21.16 -      val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
   21.17 +      val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
   21.18      in case T
   21.19 -     of Type ("fun", [_, T']) =>
   21.20 +     of Type ("fun", [_, T']) =>  (* FIXME @{type_syntax} *)
   21.21           if not (! show_types) andalso can Term.dest_Type T' then t'
   21.22           else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
   21.23        | T' => if T' = dummyT then t' else raise Match
    22.1 --- a/src/Sequents/ILL.thy	Thu Feb 11 22:06:37 2010 +0100
    22.2 +++ b/src/Sequents/ILL.thy	Thu Feb 11 22:19:58 2010 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      Sequents/ILL.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Sara Kalvala and Valeria de Paiva
    22.7      Copyright   1995  University of Cambridge
    22.8  *)
    22.9 @@ -32,19 +31,21 @@
   22.10    PromAux :: "three_seqi"
   22.11  
   22.12  syntax
   22.13 -  "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
   22.14 -  "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
   22.15 -  "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
   22.16 +  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
   22.17 +  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
   22.18 +  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
   22.19  
   22.20  parse_translation {*
   22.21 -  [("@Trueprop", single_tr "Trueprop"),
   22.22 -   ("@Context", two_seq_tr "Context"),
   22.23 -   ("@PromAux", three_seq_tr "PromAux")] *}
   22.24 +  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
   22.25 +   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
   22.26 +   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
   22.27 +*}
   22.28  
   22.29  print_translation {*
   22.30 -  [("Trueprop", single_tr' "@Trueprop"),
   22.31 -   ("Context", two_seq_tr'"@Context"),
   22.32 -   ("PromAux", three_seq_tr'"@PromAux")] *}
   22.33 +  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
   22.34 +   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
   22.35 +   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
   22.36 +*}
   22.37  
   22.38  defs
   22.39  
    23.1 --- a/src/Sequents/LK0.thy	Thu Feb 11 22:06:37 2010 +0100
    23.2 +++ b/src/Sequents/LK0.thy	Thu Feb 11 22:19:58 2010 +0100
    23.3 @@ -1,10 +1,9 @@
    23.4  (*  Title:      LK/LK0.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7      Copyright   1993  University of Cambridge
    23.8  
    23.9  There may be printing problems if a seqent is in expanded normal form
   23.10 -        (eta-expanded, beta-contracted)
   23.11 +(eta-expanded, beta-contracted).
   23.12  *)
   23.13  
   23.14  header {* Classical First-Order Sequent Calculus *}
   23.15 @@ -35,10 +34,10 @@
   23.16    Ex           :: "('a => o) => o"   (binder "EX " 10)
   23.17  
   23.18  syntax
   23.19 - "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
   23.20 + "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
   23.21  
   23.22 -parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
   23.23 -print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
   23.24 +parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
   23.25 +print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
   23.26  
   23.27  abbreviation
   23.28    not_equal  (infixl "~=" 50) where
    24.1 --- a/src/Sequents/Modal0.thy	Thu Feb 11 22:06:37 2010 +0100
    24.2 +++ b/src/Sequents/Modal0.thy	Thu Feb 11 22:19:58 2010 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      Sequents/Modal0.thy
    24.5 -    ID:         $Id$
    24.6      Author:     Martin Coen
    24.7      Copyright   1991  University of Cambridge
    24.8  *)
    24.9 @@ -18,21 +17,23 @@
   24.10    Rstar         :: "two_seqi"
   24.11  
   24.12  syntax
   24.13 -  "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   24.14 -  "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
   24.15 +  "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   24.16 +  "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
   24.17  
   24.18  ML {*
   24.19 -  val Lstar = "Lstar";
   24.20 -  val Rstar = "Rstar";
   24.21 -  val SLstar = "@Lstar";
   24.22 -  val SRstar = "@Rstar";
   24.23 -
   24.24 -  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
   24.25 -  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
   24.26 +  fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
   24.27 +  fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
   24.28  *}
   24.29  
   24.30 -parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
   24.31 -print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
   24.32 +parse_translation {*
   24.33 + [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
   24.34 +  (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
   24.35 +*}
   24.36 +
   24.37 +print_translation {*
   24.38 + [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
   24.39 +  (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
   24.40 +*}
   24.41  
   24.42  defs
   24.43    strimp_def:    "P --< Q == [](P --> Q)"
    25.1 --- a/src/Sequents/S43.thy	Thu Feb 11 22:06:37 2010 +0100
    25.2 +++ b/src/Sequents/S43.thy	Thu Feb 11 22:19:58 2010 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      Modal/S43.thy
    25.5 -    ID:         $Id$
    25.6      Author:     Martin Coen
    25.7      Copyright   1991  University of Cambridge
    25.8  
    25.9 @@ -14,25 +13,24 @@
   25.10    S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
   25.11               seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   25.12  syntax
   25.13 -  "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
   25.14 +  "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
   25.15                           ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
   25.16  
   25.17 -ML {*
   25.18 -  val S43pi  = "S43pi";
   25.19 -  val SS43pi = "@S43pi";
   25.20 -
   25.21 -  val tr  = seq_tr;
   25.22 -  val tr' = seq_tr';
   25.23 -
   25.24 -  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
   25.25 -        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   25.26 -  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
   25.27 -        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
   25.28 -
   25.29 +parse_translation {*
   25.30 +  let
   25.31 +    val tr  = seq_tr;
   25.32 +    fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
   25.33 +      Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
   25.34 +  in [(@{syntax_const "_S43pi"}, s43pi_tr)] end
   25.35  *}
   25.36  
   25.37 -parse_translation {* [(SS43pi,s43pi_tr)] *}
   25.38 -print_translation {* [(S43pi,s43pi_tr')] *}
   25.39 +print_translation {*
   25.40 +let
   25.41 +  val tr' = seq_tr';
   25.42 +  fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
   25.43 +    Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
   25.44 +in [(@{const_syntax S43pi}, s43pi_tr')] end
   25.45 +*}
   25.46  
   25.47  axioms
   25.48  (* Definition of the star operation using a set of Horn clauses  *)
    26.1 --- a/src/Sequents/Sequents.thy	Thu Feb 11 22:06:37 2010 +0100
    26.2 +++ b/src/Sequents/Sequents.thy	Thu Feb 11 22:19:58 2010 +0100
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      Sequents/Sequents.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7      Copyright   1993  University of Cambridge
    26.8  *)
    26.9 @@ -36,14 +35,14 @@
   26.10  
   26.11  
   26.12  syntax
   26.13 - SeqEmp         :: seq                                  ("")
   26.14 - SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
   26.15 + "_SeqEmp"         :: seq                                  ("")
   26.16 + "_SeqApp"         :: "[seqobj,seqcont] => seq"            ("__")
   26.17  
   26.18 - SeqContEmp     :: seqcont                              ("")
   26.19 - SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
   26.20 + "_SeqContEmp"     :: seqcont                              ("")
   26.21 + "_SeqContApp"     :: "[seqobj,seqcont] => seqcont"        (",/ __")
   26.22  
   26.23 - SeqO           :: "o => seqobj"                        ("_")
   26.24 - SeqId          :: "'a => seqobj"                       ("$_")
   26.25 + "_SeqO"           :: "o => seqobj"                        ("_")
   26.26 + "_SeqId"          :: "'a => seqobj"                       ("$_")
   26.27  
   26.28  types
   26.29   single_seqe = "[seq,seqobj] => prop"
   26.30 @@ -60,86 +59,76 @@
   26.31  
   26.32  syntax
   26.33    (*Constant to allow definitions of SEQUENCES of formulas*)
   26.34 -  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
   26.35 +  "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
   26.36  
   26.37  ML {*
   26.38  
   26.39  (* parse translation for sequences *)
   26.40  
   26.41 -fun abs_seq' t = Abs("s", Type("seq'",[]), t);
   26.42 +fun abs_seq' t = Abs ("s", Type ("seq'", []), t);   (* FIXME @{type_syntax} *)
   26.43  
   26.44 -fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
   26.45 -    seqobj_tr(_ $ i) = i;
   26.46 -
   26.47 -fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
   26.48 -    seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
   26.49 -      (seqobj_tr so) $ (seqcont_tr sc);
   26.50 +fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
   26.51 +      Const (@{const_syntax SeqO'}, dummyT) $ f
   26.52 +  | seqobj_tr (_ $ i) = i;
   26.53  
   26.54 -fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
   26.55 -    seq_tr(Const("SeqApp",_) $ so $ sc) =
   26.56 -      abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
   26.57 +fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
   26.58 +  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
   26.59 +      seqobj_tr so $ seqcont_tr sc;
   26.60  
   26.61 +fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
   26.62 +  | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
   26.63 +      abs_seq'(seqobj_tr so $ seqcont_tr sc);
   26.64  
   26.65 -fun singlobj_tr(Const("SeqO",_) $ f) =
   26.66 -    abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
   26.67 -
   26.68 +fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
   26.69 +  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
   26.70  
   26.71  
   26.72  (* print translation for sequences *)
   26.73  
   26.74  fun seqcont_tr' (Bound 0) =
   26.75 -      Const("SeqContEmp",dummyT) |
   26.76 -    seqcont_tr' (Const("SeqO'",_) $ f $ s) =
   26.77 -      Const("SeqContApp",dummyT) $
   26.78 -      (Const("SeqO",dummyT) $ f) $
   26.79 -      (seqcont_tr' s) |
   26.80 -(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
   26.81 -      seqcont_tr'(Term.betapply(a,s)) | *)
   26.82 -    seqcont_tr' (i $ s) =
   26.83 -      Const("SeqContApp",dummyT) $
   26.84 -      (Const("SeqId",dummyT) $ i) $
   26.85 -      (seqcont_tr' s);
   26.86 +      Const (@{syntax_const "_SeqContEmp"}, dummyT)
   26.87 +  | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
   26.88 +      Const (@{syntax_const "_SeqContApp"}, dummyT) $
   26.89 +        (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
   26.90 +  | seqcont_tr' (i $ s) =
   26.91 +      Const (@{syntax_const "_SeqContApp"}, dummyT) $
   26.92 +        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
   26.93  
   26.94  fun seq_tr' s =
   26.95 -    let fun seq_itr' (Bound 0) =
   26.96 -              Const("SeqEmp",dummyT) |
   26.97 -            seq_itr' (Const("SeqO'",_) $ f $ s) =
   26.98 -              Const("SeqApp",dummyT) $
   26.99 -              (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
  26.100 -(*            seq_itr' ((a as Abs(_,_,_)) $ s) =
  26.101 -              seq_itr'(Term.betapply(a,s)) |    *)
  26.102 -            seq_itr' (i $ s) =
  26.103 -              Const("SeqApp",dummyT) $
  26.104 -              (Const("SeqId",dummyT) $ i) $
  26.105 -              (seqcont_tr' s)
  26.106 -    in case s of
  26.107 -         Abs(_,_,t) => seq_itr' t |
  26.108 -         _ => s $ (Bound 0)
  26.109 -    end;
  26.110 +  let
  26.111 +    fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
  26.112 +      | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
  26.113 +          Const (@{syntax_const "_SeqApp"}, dummyT) $
  26.114 +            (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
  26.115 +      | seq_itr' (i $ s) =
  26.116 +          Const (@{syntax_const "_SeqApp"}, dummyT) $
  26.117 +            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
  26.118 +  in
  26.119 +    case s of
  26.120 +      Abs (_, _, t) => seq_itr' t
  26.121 +    | _ => s $ Bound 0
  26.122 +  end;
  26.123  
  26.124  
  26.125 +fun single_tr c [s1, s2] =
  26.126 +  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
  26.127 +
  26.128 +fun two_seq_tr c [s1, s2] =
  26.129 +  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
  26.130 +
  26.131 +fun three_seq_tr c [s1, s2, s3] =
  26.132 +  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
  26.133 +
  26.134 +fun four_seq_tr c [s1, s2, s3, s4] =
  26.135 +  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
  26.136  
  26.137  
  26.138 -fun single_tr c [s1,s2] =
  26.139 -    Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
  26.140 -
  26.141 -fun two_seq_tr c [s1,s2] =
  26.142 -    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
  26.143 -
  26.144 -fun three_seq_tr c [s1,s2,s3] =
  26.145 -    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
  26.146 -
  26.147 -fun four_seq_tr c [s1,s2,s3,s4] =
  26.148 -    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
  26.149 -
  26.150 -
  26.151 -fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
  26.152 -    singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
  26.153 +fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
  26.154 +  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
  26.155  
  26.156  
  26.157  fun single_tr' c [s1, s2] =
  26.158 -(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
  26.159 -
  26.160 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
  26.161  
  26.162  fun two_seq_tr' c [s1, s2] =
  26.163    Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
  26.164 @@ -157,7 +146,7 @@
  26.165  fun side_tr [s1] = seq_tr s1;
  26.166  *}
  26.167  
  26.168 -parse_translation {* [("@Side", side_tr)] *}
  26.169 +parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
  26.170  
  26.171  use "prover.ML"
  26.172