--- a/src/HOL/Nominal/nominal_permeq.ML Thu Apr 26 13:33:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Apr 26 14:24:08 2007 +0200
@@ -55,7 +55,7 @@
val not_false = thm "not_False_eq_True"
val perm_fun_def = thm "Nominal.perm_fun_def"
val perm_eq_app = thm "Nominal.pt_fun_app_eq"
-val supports_def = thm "Nominal.op supports_def";
+val supports_def = thm "Nominal.supports_def";
val fresh_def = thm "Nominal.fresh_def";
val fresh_prod = thm "Nominal.fresh_prod";
val fresh_unit = thm "Nominal.fresh_unit";