# HG changeset patch
# User paulson
# Date 978346324 -3600
# Node ID 9d766f21cf415852d52a30e83edfe890666cec15
# Parent  8cd507be713898e3fde42f6b04840b61c175da80
minor tidying of simprocs

diff -r 8cd507be7138 -r 9d766f21cf41 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Mon Jan 01 11:51:20 2001 +0100
+++ b/src/HOL/Real/real_arith.ML	Mon Jan 01 11:52:04 2001 +0100
@@ -12,7 +12,7 @@
 val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2,
              real_divide_1,real_times_divide1_eq,real_times_divide2_eq];
 
-val simprocs = [hd(rev real_cancel_numeral_factors)];
+val simprocs = [real_cancel_numeral_factors_divide];
 
 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
 
diff -r 8cd507be7138 -r 9d766f21cf41 src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Mon Jan 01 11:51:20 2001 +0100
+++ b/src/HOL/Real/real_arith0.ML	Mon Jan 01 11:52:04 2001 +0100
@@ -24,7 +24,7 @@
          real_mult_minus_1, real_mult_minus_1_right];
 
 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
-               Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*);
+               Real_Numeral_Simprocs.cancel_numerals;
 
 val mono_ss = simpset() addsimps
                 [real_add_le_mono,real_add_less_mono,