--- a/src/HOL/Int.thy Fri Mar 30 15:43:30 2012 +0200
+++ b/src/HOL/Int.thy Fri Mar 30 15:56:12 2012 +0200
@@ -844,16 +844,6 @@
"(m::'a::linordered_idom) = n") =
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
-setup {*
- Reorient_Proc.add
- (fn Const (@{const_name numeral}, _) $ _ => true
- | Const (@{const_name neg_numeral}, _) $ _ => true
- | _ => false)
-*}
-
-simproc_setup reorient_numeral
- ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
-
subsection{*Lemmas About Small Numerals*}