eliminated unnamed infixes;
authorwenzelm
Thu, 26 Apr 2007 14:25:37 +0200
changeset 22812 1fe9d6384b11
parent 22811 eb59c9b76d52
child 22813 882513df2472
eliminated unnamed infixes;
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";