src/HOL/Auth/Message.thy
changeset 22843 189e214845dd
parent 22424 8a5412121687
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Auth/Message.thy	Sun May 06 21:49:29 2007 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Sun May 06 21:49:32 2007 +0200
     1.3 @@ -857,7 +857,7 @@
     1.4    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
     1.5    alone.*)
     1.6  fun prove_simple_subgoals_tac i = 
     1.7 -    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
     1.8 +    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     1.9      ALLGOALS Asm_simp_tac
    1.10  
    1.11  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,