# HG changeset patch
# User wenzelm
# Date 964475277 -7200
# Node ID e46de4af70e41d9ca61a252c8b3687597d69cc83
# Parent  96973ec6fda45d5a08086d673650efcb92abc9eb
do not pass theory values, but sg_ref;

diff -r 96973ec6fda4 -r e46de4af70e4 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Mon Jul 24 23:47:14 2000 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Mon Jul 24 23:47:57 2000 +0200
@@ -15,7 +15,7 @@
   val ss		: simpset	(*basic simpset of object-logtic*)
   val eq_reflection	: thm		(*object-equality to meta-equality*)
 
-  val thy		: theory	(*the theory of the group*)
+  val sg_ref 		: Sign.sg_ref	(*signature of the theory of the group*)
   val T			: typ		(*the type of group elements*)
 
   val zero		: term
@@ -129,7 +129,7 @@
 
  val sum_conv = 
      Simplifier.mk_simproc "cancel_sums"
-       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
+       (map (Thm.read_cterm (Sign.deref sg_ref))
 	[("x + y", Data.T), ("x - y", Data.T)])
        sum_proc;
 
@@ -188,7 +188,7 @@
 
  val rel_conv = 
      Simplifier.mk_simproc "cancel_relations"
-       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
+       (map (Thm.cterm_of (Sign.deref sg_ref) o Data.dest_eqI) eqI_rules)
        rel_proc;
 
 end;
diff -r 96973ec6fda4 -r e46de4af70e4 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Mon Jul 24 23:47:14 2000 +0200
+++ b/src/Provers/Arith/assoc_fold.ML	Mon Jul 24 23:47:57 2000 +0200
@@ -13,7 +13,7 @@
 sig
   val ss		: simpset	(*basic simpset of object-logtic*)
   val eq_reflection	: thm		(*object-equality to meta-equality*)
-  val thy		: theory	(*the operator's theory*)
+  val sg_ref 		: Sign.sg_ref	(*the operator's signature*)
   val T			: typ		(*the operator's numeric type*)
   val plus		: term		(*the operator being folded*)
   val add_ac		: thm list      (*AC-rewrites for plus*)
@@ -69,7 +69,7 @@
  
  val conv = 
      Simplifier.mk_simproc "assoc_fold"
-       [Thm.cterm_of (Theory.sign_of Data.thy)
+       [Thm.cterm_of (Sign.deref Data.sg_ref)
 	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
        proc;