--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 13:59:28 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 14:05:31 2011 +0200
@@ -115,13 +115,13 @@
in
[(@{const_syntax Collect}, assert_tr'),
(@{const_syntax Basic}, assign_tr'),
- (@{const_syntax Cond}, bexp_tr' "_Cond"),
- (@{const_syntax While}, bexp_tr' "_While_inv"),
+ (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
+ (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}),
(@{const_syntax AnnBasic}, annassign_tr'),
- (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"),
- (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"),
- (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"),
- (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")]
+ (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}),
+ (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}),
+ (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}),
+ (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})]
end;
*}