src/HOL/Tools/arith_data.ML
changeset 29302 eb782d1dc07c
parent 28952 15a4b2cf8c34
child 30496 7cdcc9dd95cb
--- a/src/HOL/Tools/arith_data.ML	Thu Jan 01 22:57:42 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Thu Jan 01 23:31:49 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/arith_data.ML
-    ID:         $Id$
     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
 
 Basic arithmetic proof tools.
@@ -7,9 +6,8 @@
 
 signature ARITH_DATA =
 sig
-  val prove_conv: tactic -> (MetaSimplifier.simpset -> tactic)
-    -> MetaSimplifier.simpset -> term * term -> thm
-  val simp_all_tac: thm list -> MetaSimplifier.simpset -> tactic
+  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
+  val simp_all_tac: thm list -> simpset -> tactic
 
   val mk_sum: term list -> term
   val mk_norm_sum: term list -> term