src/HOL/Nominal/nominal_atoms.ML
changeset 22535 cbee450f88a6
parent 22418 49e2d9744ae1
child 22536 35debf264656
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:13:28 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:39:40 2007 +0200
     1.3 @@ -700,6 +700,7 @@
     1.4         val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
     1.5         val fresh_aux           = thm "Nominal.pt_fresh_aux";
     1.6         val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
     1.7 +       val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
     1.8         val set_eqvt            = thm "Nominal.pt_set_eqvt";
     1.9         val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
    1.10         val in_eqvt             = thm "Nominal.pt_in_eqvt";
    1.11 @@ -837,7 +838,8 @@
    1.12  	      in [(("fresh_bij", thms1 @ thms2),[])] end
    1.13              ||>> PureThy.add_thmss
    1.14  	      let val thms1 = inst_pt_at [fresh_eqvt]
    1.15 -	      in [(("fresh_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    1.16 +                  and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
    1.17 +	      in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
    1.18              ||>> PureThy.add_thmss
    1.19  	      let val thms1 = inst_pt_at [in_eqvt]
    1.20  	      in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end