# HG changeset patch
# User wenzelm
# Date 1177590337 -7200
# Node ID 1fe9d6384b114364362ade57b065def626aa5928
# Parent  eb59c9b76d52a1ce63d239f36b375ace2a26ae92
eliminated unnamed infixes;

diff -r eb59c9b76d52 -r 1fe9d6384b11 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 26 14:24:14 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 26 14:25:37 2007 +0200
@@ -209,7 +209,7 @@
 val supp_prod = thm "supp_prod";
 val fresh_prod = thm "fresh_prod";
 val supports_fresh = thm "supports_fresh";
-val supports_def = thm "Nominal.op supports_def";
+val supports_def = thm "Nominal.supports_def";
 val fresh_def = thm "fresh_def";
 val supp_def = thm "supp_def";
 val rev_simps = thms "rev.simps";