# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322300674 0
# Node ID a06de111c70e9a12aa0344856490a8d8129e719e
# Parent  7519ebb4114590961aa7b02a4a2f2c528b54384e
updated to Isabelle 26 Nov

diff -r 7519ebb41145 -r a06de111c70e Nominal/Nominal2_Base.thy
--- 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