# HG changeset patch
# User wenzelm
# Date 1028743418 -7200
# Node ID 459ac22f47ff824de1b48fdc010df1fcca6db8a1
# Parent  f326c5d97d767946fc748465309697a238c4d842
tuned;

diff -r f326c5d97d76 -r 459ac22f47ff src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Aug 07 20:03:17 2002 +0200
+++ b/src/Provers/simplifier.ML	Wed Aug 07 20:03:38 2002 +0200
@@ -16,10 +16,6 @@
   type simproc
   val mk_simproc: string -> cterm list
     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  val simproc: Sign.sg -> string -> string list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  val simproc_i: Sign.sg -> string -> term list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   type solver
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
   type simpset
@@ -91,6 +87,10 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val simproc: Sign.sg -> string -> string list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val simproc_i: Sign.sg -> string -> term list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   val          rewrite: simpset -> cterm -> thm
   val      asm_rewrite: simpset -> cterm -> thm
   val     full_rewrite: simpset -> cterm -> thm