# HG changeset patch
# User wenzelm
# Date 1373753295 -7200
# Node ID 06653152ea8b9eab99615f7e3d0cf74be7a83f53
# Parent  0589394aaaa5d78ed2b98677fb7efa6c2fd0b7d1
recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;

diff -r 0589394aaaa5 -r 06653152ea8b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jul 13 21:02:41 2013 +0200
+++ b/src/HOL/HOL.thy	Sun Jul 14 00:08:15 2013 +0200
@@ -1994,8 +1994,12 @@
   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
 end;
 
-fun nnf_conv ctxt =
-  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms nnf_simps});
+local
+  val nnf_ss =
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
+in
+  fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
+end
 *}
 
 hide_const (open) eq equal