# HG changeset patch
# User wenzelm
# Date 1089308096 -7200
# Node ID d23887300b9672abc19a4c979351460e0d547947
# Parent  60240294bbd571ebc3bb616be4d7a920b40bef37
adapted type of simprocs;

diff -r 60240294bbd5 -r d23887300b96 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Thu Jul 08 19:34:18 2004 +0200
+++ b/doc-src/Ref/simplifier.tex	Thu Jul 08 19:34:56 2004 +0200
@@ -1143,9 +1143,9 @@
 \section{*Coding simplification procedures}
 \begin{ttbox}
   val Simplifier.simproc: Sign.sg -> string -> string list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   val Simplifier.simproc_i: Sign.sg -> string -> term list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
 \end{ttbox}
 
 \begin{ttdescription}
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -125,7 +125,7 @@
 
  val sum_conv =
      Simplifier.mk_simproc "cancel_sums"
-       (map (Thm.read_cterm (Sign.deref sg_ref))
+       (map (Thm.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
         [("x + y", Data.T), ("x - y", Data.T)])  (* FIXME depends on concrete syntax !???!!??! *)
        sum_proc;
 
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -28,7 +28,7 @@
 
 signature CANCEL_DIV_MOD =
 sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
 end;
 
 
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -40,7 +40,7 @@
 
 functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
   sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
   end 
 =
 struct
@@ -51,8 +51,10 @@
   | gcd (m, n) = gcd (n mod m, m);
 
 (*the simplification procedure*)
-fun proc sg hyps t =
-  let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+  let
+      val hyps = prems_of_ss ss;
+      (*first freeze any Vars in the term to prevent flex-flex problems*)
       val (t', xs) = Term.adhoc_freeze_vars t;
       val (t1,t2) = Data.dest_bal t' 
       val (m1, t1') = Data.dest_coeff t1
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -47,7 +47,7 @@
 
 functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
   sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
   end 
 =
 struct
@@ -69,8 +69,10 @@
   in  seek terms1 end;
 
 (*the simplification procedure*)
-fun proc sg hyps t =
-  let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+  let
+      val hyps = prems_of_ss ss;
+      (*first freeze any Vars in the term to prevent flex-flex problems*)
       val (t', xs) = Term.adhoc_freeze_vars t;
       val (t1,t2) = Data.dest_bal t' 
       val terms1 = Data.dest_sum t1
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_sums.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -24,7 +24,7 @@
 
 signature CANCEL_SUMS =
 sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
 end;
 
 
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -37,7 +37,7 @@
 
 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
   sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
   end 
 =
 struct
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -32,7 +32,7 @@
 
 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
   sig
-  val proc: Sign.sg -> thm list -> term -> thm option
+  val proc: Sign.sg -> simpset -> term -> thm option
   end 
 =
 struct
@@ -50,8 +50,10 @@
   in  seek terms1 end;
 
 (*the simplification procedure*)
-fun proc sg hyps t =
-  let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+  let
+      val hyps = prems_of_ss ss;
+      (*first freeze any Vars in the term to prevent flex-flex problems*)
       val (t', xs) = Term.adhoc_freeze_vars t;
       val (t1,t2) = Data.dest_bal t' 
       val terms1 = Data.dest_sum t1
diff -r 60240294bbd5 -r d23887300b96 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -11,7 +11,7 @@
 
 and a simplification procedure
 
-    lin_arith_prover: Sign.sg -> thm list -> term -> thm option
+    lin_arith_prover: Sign.sg -> simpset -> term -> thm option
 
 Only take premises and conclusions into account that are already (negated)
 (in)equations. lin_arith_prover tries to prove or disprove the term.
@@ -78,7 +78,7 @@
                 -> theory -> theory
   val trace           : bool ref
   val fast_arith_neq_limit: int ref
-  val lin_arith_prover: Sign.sg -> thm list -> term -> thm option
+  val lin_arith_prover: Sign.sg -> simpset -> term -> thm option
   val     lin_arith_tac:     bool -> int -> tactic
   val cut_lin_arith_tac: thm list -> int -> tactic
 end;
@@ -714,8 +714,10 @@
    2. lin_arith_prover is applied by the simplifier which
       dives into terms and will thus try the non-negated concl anyway.
 *)
-fun lin_arith_prover sg thms concl =
-let val Hs = map (#prop o rep_thm) thms
+fun lin_arith_prover sg ss concl =
+let
+    val thms = prems_of_ss ss;
+    val Hs = map (#prop o rep_thm) thms
     val Tconcl = LA_Logic.mk_Trueprop concl
 in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
      Some js => prover sg thms Tconcl js true
diff -r 60240294bbd5 -r d23887300b96 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/quantifier1.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -57,10 +57,10 @@
 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
-  val rearrange_all: Sign.sg -> thm list -> term -> thm option
-  val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
-  val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
-  val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
+  val rearrange_all: Sign.sg -> simpset -> term -> thm option
+  val rearrange_ex:  Sign.sg -> simpset -> term -> thm option
+  val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
+  val rearrange_bex:  tactic -> Sign.sg -> simpset -> term -> thm option
 end;
 
 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =