1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:37 2008 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:39 2008 +0100
     1.3 @@ -697,7 +697,7 @@
     1.4  {*
     1.5  fun rename_client_map_tac ss =
     1.6    EVERY [
     1.7 -    simp_tac (ss addsimps [thm "rename_guarantees_eq_rename_inv"]) 1,
     1.8 +    simp_tac (ss addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
     1.9      rtac @{thm guarantees_PLam_I} 1,
    1.10      assume_tac 2,
    1.11           (*preserves: routine reasoning*)