src/HOL/Nominal/nominal_permeq.ML
changeset 19993 e0a5783d708f
parent 19987 b97607d4d9a5
child 20289 ba7a7c56bed5
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 15:57:19 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 17:26:02 2006 +0200
     1.3 @@ -271,6 +271,9 @@
     1.4      handle Subscript => Seq.empty
     1.5  
     1.6  val supports_fresh_rule = thm "supports_fresh";
     1.7 +val fresh_def           = thm "Nominal.fresh_def";
     1.8 +val fresh_prod          = thm "Nominal.fresh_prod";
     1.9 +val fresh_unit          = thm "Nominal.fresh_unit";
    1.10  
    1.11  fun fresh_guess_tac tactical ss i st =
    1.12      let 
    1.13 @@ -293,15 +296,15 @@
    1.14                Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
    1.15              val supports_fresh_rule'' = Drule.cterm_instantiate
    1.16                [(cert (head_of S), cert s')] supports_fresh_rule'
    1.17 -            val fresh_def   = thm "Nominal.fresh_def";
    1.18 -	    val fresh_prod  = thm "Nominal.fresh_prod";
    1.19 -            val fresh_unit  = thm "Nominal.fresh_unit";
    1.20 -	    val simps       = [symmetric fresh_def,fresh_prod,fresh_unit]
    1.21 +	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
    1.22 +            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
    1.23 +            (* FIXME sometimes these rewrite rules are already in the ss, *)
    1.24 +            (* which produces a warning                                   *)
    1.25            in
    1.26              (tactical ("guessing of the right set that supports the goal",
    1.27                        EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
    1.28 -                             asm_full_simp_tac (ss addsimps simps) (i+2),
    1.29 -                             asm_full_simp_tac ss (i+1), 
    1.30 +                             asm_full_simp_tac ss1 (i+2),
    1.31 +                             asm_full_simp_tac ss2 (i+1), 
    1.32                               supports_tac tactical ss i])) st
    1.33            end
    1.34          | _ => Seq.empty