--- a/src/HOL/Tools/lin_arith.ML Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Nov 24 21:01:06 2011 +0100
@@ -704,8 +704,9 @@
local
val nnf_simpset =
- empty_ss setmkeqTrue mk_eq_True
- setmksimps (mksimps mksimps_pairs)
+ (empty_ss
+ |> Simplifier.set_mkeqTrue mk_eq_True
+ |> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
@{thm de_Morgan_conj}, not_all, not_ex, not_not]
fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
@@ -838,8 +839,9 @@
local
val nnf_simpset =
- empty_ss setmkeqTrue mk_eq_True
- setmksimps (mksimps mksimps_pairs)
+ (empty_ss
+ |> Simplifier.set_mkeqTrue mk_eq_True
+ |> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
@{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
fun prem_nnf_tac i st =