src/HOL/HoareParallel/RG_Syntax.thy
changeset 22759 e4a3f49eb924
parent 22741 4bd02e03305c
child 25706 45d090186bbe
     1.1 --- a/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:24 2007 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:25 2007 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
     1.5  
     1.6  translations
     1.7 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
     1.8 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
     1.9    "SKIP" \<rightleftharpoons> "Basic id"
    1.10    "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
    1.11    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    1.12 @@ -78,7 +78,7 @@
    1.13        | update_name_tr' (Const x) = Const (upd_tr' x)
    1.14        | update_name_tr' _ = raise Match;
    1.15  
    1.16 -    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    1.17 +    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"}, _)$t) $ Bound 0) :: ts) =
    1.18            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    1.19              (Abs (x, dummyT, t) :: ts)
    1.20        | assign_tr' _ = raise Match;