--- a/src/HOL/HoareParallel/OG_Syntax.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/HoareParallel/OG_Syntax.thy Wed Dec 19 16:32:14 2007 +0100
@@ -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 (\<lambda>_. a))\<guillemotright>"
+ "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
syntax
"_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
@@ -105,14 +105,18 @@
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
+ fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' _ = raise Match;
+
+ fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
- fun annassign_tr' (r :: Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
+ fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| annassign_tr' _ = raise Match;
fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] =