# HG changeset patch
# User haftmann
# Date 1177060899 -7200
# Node ID 4bd02e03305c0f52ce3efee50b19779fc1d826df
# Parent  2d8d0d61475aa4e1ea9d2cdd459b0cb21cc3897f
tuned syntax: K_record is now an authentic constant

diff -r 2d8d0d61475a -r 4bd02e03305c src/HOL/HoareParallel/OG_Syntax.thy
--- a/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 11:21:38 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 11:21:39 2007 +0200
@@ -10,8 +10,8 @@
   "_AnnAssign"   :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
-  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
+  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
+  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
 
 syntax
   "_AnnSkip"     :: "'a assn \<Rightarrow> 'a ann_com"              ("_//SKIP" [90] 63)
@@ -105,12 +105,12 @@
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
 
-    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
+    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
           quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
             (Abs (x, dummyT, t) :: ts)
       | assign_tr' _ = raise Match;
 
-    fun annassign_tr' (r :: Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
+    fun annassign_tr' (r :: Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
           quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
             (Abs (x, dummyT, t) :: ts)
       | annassign_tr' _ = raise Match;
diff -r 2d8d0d61475a -r 4bd02e03305c src/HOL/HoareParallel/RG_Syntax.thy
--- a/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 11:21:38 2007 +0200
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 11:21:39 2007 +0200
@@ -16,7 +16,7 @@
   "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
+  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
   "SKIP" \<rightleftharpoons> "Basic id"
   "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
diff -r 2d8d0d61475a -r 4bd02e03305c src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 11:21:38 2007 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 11:21:39 2007 +0200
@@ -228,8 +228,8 @@
 
 translations
   ".{b}."                   => "Collect .(b)."
-  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
-  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (K_record a)))."
+  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (CONST K_record a)) \<in> B}."
+  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (CONST K_record a)))."
   "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
   "WHILE b INV i DO c OD"   => "While .{b}. i c"
   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"