--- a/src/FOL/ex/IffOracle.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/FOL/ex/IffOracle.ML Wed Mar 17 16:33:47 1999 +0100
@@ -7,7 +7,7 @@
*)
fun iff_oracle n =
- invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
+ invoke_oracle IffOracle.thy "iff" (Theory.sign_of IffOracle.thy, IffOracleExn n);
iff_oracle 2;
--- a/src/FOL/simpdata.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/FOL/simpdata.ML Wed Mar 17 16:33:47 1999 +0100
@@ -243,10 +243,10 @@
local
val ex_pattern =
- read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
+ read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
val all_pattern =
- read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
+ read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
in
val defEX_regroup =
--- a/src/Provers/Arith/abel_cancel.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Wed Mar 17 16:33:47 1999 +0100
@@ -128,7 +128,7 @@
val sum_conv =
Simplifier.mk_simproc "cancel_sums"
- (map (Thm.read_cterm (sign_of Data.thy))
+ (map (Thm.read_cterm (Theory.sign_of Data.thy))
[("x + y", Data.T), ("x - y", Data.T)])
sum_proc;
@@ -187,7 +187,7 @@
val rel_conv =
Simplifier.mk_simproc "cancel_relations"
- (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
+ (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
rel_proc;
end;
--- a/src/Provers/blast.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/Provers/blast.ML Wed Mar 17 16:33:47 1999 +0100
@@ -1319,10 +1319,10 @@
fun tryInThy thy lim s =
(initialize();
- timeap prove (sign_of thy,
+ timeap prove (Theory.sign_of thy,
startTiming(),
Data.claset(),
- [initBranch ([readGoal (sign_of thy) s], lim)],
+ [initBranch ([readGoal (Theory.sign_of thy) s], lim)],
I));
--- a/src/Provers/classical.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/Provers/classical.ML Wed Mar 17 16:33:47 1999 +0100
@@ -807,15 +807,15 @@
val claset_ref_of_sg = Sign.get_data clasetK (fn ClasetData (ref (CSData r)) => r);
-val claset_ref_of = claset_ref_of_sg o sign_of;
+val claset_ref_of = claset_ref_of_sg o Theory.sign_of;
val claset_of_sg = ! o claset_ref_of_sg;
-val claset_of = claset_of_sg o sign_of;
+val claset_of = claset_of_sg o Theory.sign_of;
-fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state;
-fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state;
+fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
+fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
val claset = claset_of o Context.the_context;
-val claset_ref = claset_ref_of_sg o sign_of o Context.the_context;
+val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
(* change claset *)
--- a/src/Provers/simplifier.ML Wed Mar 17 16:33:00 1999 +0100
+++ b/src/Provers/simplifier.ML Wed Mar 17 16:33:47 1999 +0100
@@ -280,13 +280,13 @@
(* access global simpset *)
val simpset_of_sg = ! o simpset_ref_of_sg;
-val simpset_of = simpset_of_sg o sign_of;
+val simpset_of = simpset_of_sg o Theory.sign_of;
-fun SIMPSET tacf state = tacf (simpset_of_sg (sign_of_thm state)) state;
-fun SIMPSET' tacf i state = tacf (simpset_of_sg (sign_of_thm state)) i state;
+fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
+fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
val simpset = simpset_of o Context.the_context;
-val simpset_ref = simpset_ref_of_sg o sign_of o Context.the_context;
+val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
(* change global simpset *)