| changeset 22812 | 1fe9d6384b11 |
| parent 22675 | acf10be7dcca |
| child 22846 | fb79144af9a3 |
--- 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";