--- a/src/HOL/Nominal/nominal_atoms.ML Tue Jul 04 15:57:19 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jul 04 17:26:02 2006 +0200
@@ -773,9 +773,7 @@
in [(("fresh_atm", thms1 @ thms2),[])] end
||>> PureThy.add_thmss
let val thms1 = List.concat (List.concat perm_defs)
- val thms2 = List.concat prm_eqs
- val thms3 = List.concat swap_eqs
- in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end
+ in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [abs_fun_pi]
and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]