# HG changeset patch
# User wenzelm
# Date 1302264331 -7200
# Node ID 24075ad39ca24fc92b0ee3d9df0e72ac4192f1f5
# Parent  8d91a85b6d916700e0ba17311005dfba8a4de5f2
more antiquotations;

diff -r 8d91a85b6d91 -r 24075ad39ca2 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- 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;
 *}