src/HOL/Auth/Message.thy
changeset 26342 0f65fa163304
parent 24122 fc7f857d33c8
child 26807 4cd176ea28dc
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -847,8 +847,8 @@
     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 [@{thm image_eq_UN}]) i THEN
     1.8 -    ALLGOALS Asm_simp_tac
     1.9 +    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
    1.10 +    ALLGOALS (SIMPSET' asm_simp_tac)
    1.11  
    1.12  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    1.13    but this application is no longer necessary if analz_insert_eq is used.
    1.14 @@ -886,7 +886,7 @@
    1.15         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.16         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.17  
    1.18 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    1.19 +val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
    1.20  
    1.21  end
    1.22  *}