--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 13:31:16 2011 +0200
@@ -76,11 +76,11 @@
print_translation {*
let
fun quote_tr' f (t :: ts) =
- Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+ Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
| quote_tr' _ _ = raise Match;
fun annquote_tr' f (r :: t :: ts) =
- Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+ Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
| annquote_tr' _ _ = raise Match;
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -94,13 +94,13 @@
| annbexp_tr' _ _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+ quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
+ (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+ quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
+ (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| annassign_tr' _ = raise Match;
fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $