recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
authorwenzelm
Sun Jul 14 00:08:15 2013 +0200 (2013-07-14)
changeset 5265406653152ea8b
parent 52653 0589394aaaa5
child 52655 3b2b1ef13979
recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 13 21:02:41 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jul 14 00:08:15 2013 +0200
     1.3 @@ -1994,8 +1994,12 @@
     1.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
     1.5  end;
     1.6  
     1.7 -fun nnf_conv ctxt =
     1.8 -  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms nnf_simps});
     1.9 +local
    1.10 +  val nnf_ss =
    1.11 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
    1.12 +in
    1.13 +  fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
    1.14 +end
    1.15  *}
    1.16  
    1.17  hide_const (open) eq equal