# HG changeset patch
# User wenzelm
# Date 1201468899 -3600
# Node ID 21b51f748dafeefcbdacf4795fe42dec1adba2b4
# Parent  d35484265f46fd6091c694f60b856b378d0ea3ab
rename_client_map_tac: avoid ill-defined thm reference;

diff -r d35484265f46 -r 21b51f748daf src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:37 2008 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Jan 27 22:21:39 2008 +0100
@@ -697,7 +697,7 @@
 {*
 fun rename_client_map_tac ss =
   EVERY [
-    simp_tac (ss addsimps [thm "rename_guarantees_eq_rename_inv"]) 1,
+    simp_tac (ss addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
     rtac @{thm guarantees_PLam_I} 1,
     assume_tac 2,
          (*preserves: routine reasoning*)