src/HOL/Nominal/nominal_permeq.ML
changeset 22565 2a1eef99bb6a
parent 22562 80b814fe284b
child 22578 b0eb5652f210
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Apr 03 16:20:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Apr 03 17:05:52 2007 +0200
@@ -54,7 +54,6 @@
 val conj_absorb   = thm "conj_absorb";
 val not_false     = thm "not_False_eq_True"
 val perm_fun_def  = thm "Nominal.perm_fun_def"
-val swap_fun      = thm "Nominal.swap_fun" (* FIXME: is this still needed? *)
 val perm_eq_app   = thm "Nominal.pt_fun_app_eq"
 val supports_def  = thm "Nominal.op supports_def";
 val fresh_def     = thm "Nominal.fresh_def";