diff -r 2ba15af46cb7 -r 74bf78db0d87 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Mar 26 12:01:40 2011 +0100
@@ -67,15 +67,9 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    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 @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, K_tr' k) :: ts)
+            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),