src/HOL/Nominal/nominal_atoms.ML
changeset 18626 b6596f579e40
parent 18600 20ad06db427b
child 18651 0cb5a8f501aa
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Jan 09 13:29:08 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jan 09 15:55:15 2006 +0100
     1.3 @@ -750,8 +750,9 @@
     1.4                in [(("perm_dj", thms1 @ thms2),[])] end
     1.5              ||>> PureThy.add_thmss
     1.6  	      let val thms1 = inst_pt_at_fs [fresh_iff]
     1.7 -		  and thms2 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
     1.8 -	    in [(("abs_fresh", thms1 @ thms2),[])] end
     1.9 +                  and thms2 = inst_pt_at [fresh_iff]
    1.10 +		  and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
    1.11 +	    in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end
    1.12  	    ||>> PureThy.add_thmss
    1.13  	      let val thms1 = inst_pt_at [abs_fun_supp]
    1.14  		  and thms2 = inst_pt_at_fs [abs_fun_supp]