src/HOL/Nominal/Nominal.thy
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 *}