--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 13:31:16 2011 +0200
@@ -58,7 +58,7 @@
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;
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -68,8 +68,8 @@
| bexp_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;
in
[(@{const_syntax Collect}, assert_tr'),