# HG changeset patch
# User wenzelm
# Date 921684827 -3600
# Node ID 0da748358eff06f7a12ce725ae513aa71db74db5
# Parent  5d58c100ca3fdafa2c8b1582dffc9a7a7806ee03
Theory.sign_of;

diff -r 5d58c100ca3f -r 0da748358eff src/FOL/ex/IffOracle.ML
--- 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;
diff -r 5d58c100ca3f -r 0da748358eff src/FOL/simpdata.ML
--- 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 =
diff -r 5d58c100ca3f -r 0da748358eff src/Provers/Arith/abel_cancel.ML
--- 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;
diff -r 5d58c100ca3f -r 0da748358eff src/Provers/blast.ML
--- 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));
 
 
diff -r 5d58c100ca3f -r 0da748358eff src/Provers/classical.ML
--- 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 *)
diff -r 5d58c100ca3f -r 0da748358eff src/Provers/simplifier.ML
--- 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 *)