1.1 --- a/src/HOL/Int.thy	Fri Mar 30 15:43:30 2012 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri Mar 30 15:56:12 2012 +0200
     1.3 @@ -844,16 +844,6 @@
     1.4    "(m::'a::linordered_idom) = n") =
     1.5    {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
     1.6  
     1.7 -setup {*
     1.8 -  Reorient_Proc.add
     1.9 -    (fn Const (@{const_name numeral}, _) $ _ => true
    1.10 -    | Const (@{const_name neg_numeral}, _) $ _ => true
    1.11 -    | _ => false)
    1.12 -*}
    1.13 -
    1.14 -simproc_setup reorient_numeral
    1.15 -  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
    1.16 -
    1.17  
    1.18  subsection{*Lemmas About Small Numerals*}
    1.19  

     2.1 --- a/src/HOL/Num.thy	Fri Mar 30 15:43:30 2012 +0200
     2.2 +++ b/src/HOL/Num.thy	Fri Mar 30 15:56:12 2012 +0200
     2.3 @@ -975,10 +975,6 @@
     2.4  
     2.5  subsection {* Setting up simprocs *}
     2.6  
     2.7 -lemma numeral_reorient:
     2.8 -  "(numeral w = x) = (x = numeral w)"
     2.9 -  by auto
    2.10 -
    2.11  lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"
    2.12    by simp
    2.13  
    2.14 @@ -999,6 +995,16 @@
    2.15    mult_numeral_1 mult_numeral_1_right 
    2.16    mult_minus1 mult_minus1_right
    2.17  
    2.18 +setup {*
    2.19 +  Reorient_Proc.add
    2.20 +    (fn Const (@{const_name numeral}, _) $ _ => true
    2.21 +    | Const (@{const_name neg_numeral}, _) $ _ => true
    2.22 +    | _ => false)
    2.23 +*}
    2.24 +
    2.25 +simproc_setup reorient_numeral
    2.26 +  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
    2.27 +
    2.28  
    2.29  subsubsection {* Simplification of arithmetic operations on integer constants. *}
    2.30