--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat May 25 15:37:53 2013 +0200
@@ -72,10 +72,10 @@
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
- [(@{const_syntax Collect}, assert_tr'),
- (@{const_syntax Basic}, assign_tr'),
- (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
- (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
+ [(@{const_syntax Collect}, K assert_tr'),
+ (@{const_syntax Basic}, K assign_tr'),
+ (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
+ (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))]
end
*}