# 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