--- a/Nominal/Nominal2_Base.thy	Sat Nov 26 09:24:19 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 26 09:44:34 2011 +0000
@@ -2023,12 +2023,12 @@
   and   "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
   by (simp_all add: fresh_Pair)
 
-ML {*
-  val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs;
-*}
-
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+let
+  val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs
+in
+  Simplifier.map_ss (fn ss => Simplifier.set_mksimps (mksimps mksimps_pairs) ss)
+end
 *}
 
 text {* The fresh-star generalisation of fresh is used in strong