src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Sun May 06 21:49:29 2007 +0200
+++ b/src/HOL/Auth/Message.thy	Sun May 06 21:49:32 2007 +0200
@@ -857,7 +857,7 @@
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     ALLGOALS Asm_simp_tac
 
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,