diff -r 7123ae179212 -r bb72bd43c6c3 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Thu Aug 08 23:42:49 2002 +0200
+++ b/src/HOL/Real/RealBin.ML	Thu Aug 08 23:46:09 2002 +0200
@@ -376,20 +376,6 @@
 fun trans_tac None      = all_tac
   | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
 
-fun prove_conv name tacs sg (hyps: thm list) (t,u) =
-  if t aconv u then None
-  else
-  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
-  in Some
-     (prove_goalw_cterm [] ct (K tacs)
-      handle ERROR => error
-          ("The error(s) above occurred while trying to prove " ^
-           string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
-  end;
-
-(*version without the hyps argument*)
-fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
-
 (*Final simplification: cancel + and *  *)
 val simplify_meta_eq =
     Int_Numeral_Simprocs.simplify_meta_eq
@@ -421,7 +407,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = prove_conv "realeq_cancel_numerals"
+  val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
   val bal_add1 = real_eq_add_iff1 RS trans
@@ -430,7 +416,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = prove_conv "realless_cancel_numerals"
+  val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "op <"
   val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
   val bal_add1 = real_less_add_iff1 RS trans
@@ -439,7 +425,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = prove_conv "realle_cancel_numerals"
+  val prove_conv = Bin_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "op <="
   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
   val bal_add1 = real_le_add_iff1 RS trans
@@ -473,7 +459,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val left_distrib      = left_real_add_mult_distrib RS trans
-  val prove_conv        = prove_conv_nohyps "real_combine_numerals"
+  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac         = trans_tac
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
@@ -520,7 +506,7 @@
   val is_numeral      = Bin_Simprocs.is_numeral
   val numeral_0_eq_0  = real_numeral_0_eq_0
   val numeral_1_eq_1  = real_numeral_1_eq_1
-  val prove_conv      = prove_conv_nohyps "real_abstract_numerals"
+  val prove_conv      = Bin_Simprocs.prove_conv_nohyps_novars
   fun norm_tac simps  = ALLGOALS (simp_tac (HOL_ss addsimps simps))
   val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
   end