--- a/src/HOL/Tools/nat_arith.ML Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/nat_arith.ML Wed Jul 15 23:48:21 2009 +0200
@@ -91,18 +91,18 @@
end);
val nat_cancel_sums_add =
- [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
+ [Simplifier.simproc @{theory} "nateq_cancel_sums"
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
(K EqCancelSums.proc),
- Simplifier.simproc (the_context ()) "natless_cancel_sums"
+ Simplifier.simproc @{theory} "natless_cancel_sums"
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
(K LessCancelSums.proc),
- Simplifier.simproc (the_context ()) "natle_cancel_sums"
+ Simplifier.simproc @{theory} "natle_cancel_sums"
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
(K LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
- [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
+ [Simplifier.simproc @{theory} "natdiff_cancel_sums"
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
(K DiffCancelSums.proc)];