diff -r 329bc52b4b86 -r 750c5a47400b src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -704,8 +704,9 @@
 
 local
   val nnf_simpset =
-    empty_ss setmkeqTrue mk_eq_True
-    setmksimps (mksimps mksimps_pairs)
+    (empty_ss
+      |> Simplifier.set_mkeqTrue mk_eq_True
+      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
       @{thm de_Morgan_conj}, not_all, not_ex, not_not]
   fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
@@ -838,8 +839,9 @@
 
 local
   val nnf_simpset =
-    empty_ss setmkeqTrue mk_eq_True
-    setmksimps (mksimps mksimps_pairs)
+    (empty_ss
+      |> Simplifier.set_mkeqTrue mk_eq_True
+      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
       @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
   fun prem_nnf_tac i st =