src/HOL/simpdata.ML
changeset 17892 62c397c17d18
parent 17875 d81094515061
child 17959 8db36a108213
     1.1 --- a/src/HOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
     1.3 @@ -341,7 +341,8 @@
     1.4  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
     1.5  
     1.6  val HOL_basic_ss =
     1.7 -  empty_ss setsubgoaler asm_simp_tac
     1.8 +  Simplifier.theory_context (the_context ()) empty_ss
     1.9 +    setsubgoaler asm_simp_tac
    1.10      setSSolver safe_solver
    1.11      setSolver unsafe_solver
    1.12      setmksimps (mksimps mksimps_pairs)
    1.13 @@ -460,14 +461,13 @@
    1.14  *)
    1.15  
    1.16  local
    1.17 -  val nnf_simps =
    1.18 -        [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
    1.19 -         not_all,not_ex,not_not];
    1.20    val nnf_simpset =
    1.21 -        empty_ss setmkeqTrue mk_eq_True
    1.22 -                 setmksimps (mksimps mksimps_pairs)
    1.23 -                 addsimps nnf_simps;
    1.24 -  val prem_nnf_tac = full_simp_tac nnf_simpset
    1.25 +    empty_ss setmkeqTrue mk_eq_True
    1.26 +    setmksimps (mksimps mksimps_pairs)
    1.27 +    addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
    1.28 +      not_all,not_ex,not_not];
    1.29 +  fun prem_nnf_tac i st =
    1.30 +    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
    1.31  in
    1.32  fun refute_tac test prep_tac ref_tac =
    1.33    let val refute_prems_tac =