diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 16 13:35:42 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 16 14:08:39 2010 +0100
@@ -260,23 +260,14 @@
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun upd_tr' (x_upd, T) =
-      (case try (unsuffix Record.updateN) x_upd of
-        SOME x => (x, if T = dummyT then T else Term.domain_type T)
-      | NONE => raise Match);
-
-    fun update_name_tr' (Free x) = Free (upd_tr' x)
-      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
-          c $ Free (upd_tr' x)
-      | update_name_tr' (Const x) = Const (upd_tr' x)
-      | update_name_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
+    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"} $ update_name_tr' f)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
             (Abs (x, dummyT, K_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in