--- 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;
--- 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;