# HG changeset patch
# User haftmann
# Date 1178480972 -7200
# Node ID 189e214845dd6529fdb10a07bb36e19ab3178c78
# Parent  6d2fd4e0f9844a5af4d1c8368189de7c54fe5454
dropped legacy ML binding

diff -r 6d2fd4e0f984 -r 189e214845dd 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,
diff -r 6d2fd4e0f984 -r 189e214845dd src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:29 2007 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:32 2007 +0200
@@ -844,7 +844,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,