src/CCL/Type.thy
changeset 30607 c3d1590debd8
parent 28272 ed959a0f650b
child 32010 cb1a1c94b4cd
     1.1 --- a/src/CCL/Type.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/CCL/Type.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      CCL/Type.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Martin Coen
     1.7      Copyright   1993  University of Cambridge
     1.8  *)
     1.9 @@ -409,7 +408,7 @@
    1.10  
    1.11  fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
    1.12        (fn prems => [rtac (genXH RS iffD2) 1,
    1.13 -                    SIMPSET' simp_tac 1,
    1.14 +                    simp_tac (simpset_of thy) 1,
    1.15                      TRY (fast_tac (@{claset} addIs
    1.16                              ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
    1.17                               @ prems)) 1)])
    1.18 @@ -442,8 +441,8 @@
    1.19     "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    1.20     "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
    1.21  
    1.22 -fun POgen_tac (rla,rlb) i =
    1.23 -  SELECT_GOAL (CLASET safe_tac) i THEN
    1.24 +fun POgen_tac ctxt (rla,rlb) i =
    1.25 +  SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
    1.26    rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
    1.27    (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
    1.28      (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));