# HG changeset patch
# User huffman
# Date 1319875235 -7200
# Node ID 1e380c50a183fddca7117a22035be7f7c3078298
# Parent  7a97b2bda137a8a0e6e78d73721a6682e41446d5
remove unused function

diff -r 7a97b2bda137 -r 1e380c50a183 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Oct 28 16:49:15 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Oct 29 10:00:35 2011 +0200
@@ -365,7 +365,6 @@
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq
-  val prove_conv = Arith_Data.prove_conv
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;
 
diff -r 7a97b2bda137 -r 1e380c50a183 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 28 16:49:15 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 29 10:00:35 2011 +0200
@@ -470,7 +470,6 @@
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
-  val prove_conv = Arith_Data.prove_conv
   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;
 
diff -r 7a97b2bda137 -r 1e380c50a183 src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Fri Oct 28 16:49:15 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Sat Oct 29 10:00:35 2011 +0200
@@ -23,7 +23,6 @@
   val find_first: term -> term list -> term list
   (*proof tools*)
   val mk_eq: term * term -> term
-  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val norm_tac: simpset -> tactic                (*proves the result*)
   val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
   val simp_conv: simpset -> term -> thm option  (*proves simp thm*)