recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;

--- 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