dropped legacy ML binding
authorhaftmann
Sun May 06 21:49:32 2007 +0200 (2007-05-06)
changeset 22843189e214845dd
parent 22842 6d2fd4e0f984
child 22844 91c05f4b509e
dropped legacy ML binding
src/HOL/Auth/Message.thy
src/HOL/SET-Protocol/MessageSET.thy
     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,
     2.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:29 2007 +0200
     2.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:32 2007 +0200
     2.3 @@ -844,7 +844,7 @@
     2.4    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
     2.5    alone.*)
     2.6  fun prove_simple_subgoals_tac i =
     2.7 -    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
     2.8 +    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     2.9      ALLGOALS Asm_simp_tac
    2.10  
    2.11  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,