changeset 45625 | 750c5a47400b |
parent 44838 | 096ec174be5d |
child 45694 | 4a8743618257 |
--- a/src/HOL/Nominal/Nominal.thy Thu Nov 24 20:45:34 2011 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Nov 24 21:01:06 2011 +0100 @@ -378,7 +378,7 @@ val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs; *} declaration {* fn _ => - Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) + Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) *} section {* Abstract Properties for Permutations and Atoms *}