# HG changeset patch
# User wenzelm
# Date 1393796275 -3600
# Node ID c38ad094e5bfd72f2dbcb16a68c0b87e5c432511
# Parent  b56fda32bf24dac75fe69e13b10ec934281d1b06
silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;

diff -r b56fda32bf24 -r c38ad094e5bf src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 22:24:52 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 22:37:55 2014 +0100
@@ -180,7 +180,9 @@
 
 fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
   let
-    val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+    val ctxt' =
+      Context_Position.set_visible false (put_simpset dlo_ss ctxt)
+        addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
     val dnfex_conv = Simplifier.rewrite ctxt'
     val pcv =
       Simplifier.rewrite