Theory.sign_of;
authorwenzelm
Wed Mar 17 16:33:47 1999 +0100 (1999-03-17 ago)
changeset 63910da748358eff
parent 6390 5d58c100ca3f
child 6392 e2ecfd8622ae
Theory.sign_of;
src/FOL/ex/IffOracle.ML
src/FOL/simpdata.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
     1.1 --- a/src/FOL/ex/IffOracle.ML	Wed Mar 17 16:33:00 1999 +0100
     1.2 +++ b/src/FOL/ex/IffOracle.ML	Wed Mar 17 16:33:47 1999 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  *)
     1.5  
     1.6  fun iff_oracle n =
     1.7 -  invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
     1.8 +  invoke_oracle IffOracle.thy "iff" (Theory.sign_of IffOracle.thy, IffOracleExn n);
     1.9  
    1.10  
    1.11  iff_oracle 2;
     2.1 --- a/src/FOL/simpdata.ML	Wed Mar 17 16:33:00 1999 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Wed Mar 17 16:33:47 1999 +0100
     2.3 @@ -243,10 +243,10 @@
     2.4  
     2.5  local
     2.6  val ex_pattern =
     2.7 -  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
     2.8 +  read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
     2.9  
    2.10  val all_pattern =
    2.11 -  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    2.12 +  read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    2.13  
    2.14  in
    2.15  val defEX_regroup =
     3.1 --- a/src/Provers/Arith/abel_cancel.ML	Wed Mar 17 16:33:00 1999 +0100
     3.2 +++ b/src/Provers/Arith/abel_cancel.ML	Wed Mar 17 16:33:47 1999 +0100
     3.3 @@ -128,7 +128,7 @@
     3.4  
     3.5   val sum_conv = 
     3.6       Simplifier.mk_simproc "cancel_sums"
     3.7 -       (map (Thm.read_cterm (sign_of Data.thy)) 
     3.8 +       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
     3.9  	[("x + y", Data.T), ("x - y", Data.T)])
    3.10         sum_proc;
    3.11  
    3.12 @@ -187,7 +187,7 @@
    3.13  
    3.14   val rel_conv = 
    3.15       Simplifier.mk_simproc "cancel_relations"
    3.16 -       (map (Thm.cterm_of (sign_of Data.thy) o Data.dest_eqI) eqI_rules)
    3.17 +       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI) eqI_rules)
    3.18         rel_proc;
    3.19  
    3.20  end;
     4.1 --- a/src/Provers/blast.ML	Wed Mar 17 16:33:00 1999 +0100
     4.2 +++ b/src/Provers/blast.ML	Wed Mar 17 16:33:47 1999 +0100
     4.3 @@ -1319,10 +1319,10 @@
     4.4  
     4.5  fun tryInThy thy lim s = 
     4.6      (initialize();
     4.7 -     timeap prove (sign_of thy, 
     4.8 +     timeap prove (Theory.sign_of thy, 
     4.9  		   startTiming(), 
    4.10  		   Data.claset(), 
    4.11 -		   [initBranch ([readGoal (sign_of thy) s], lim)], 
    4.12 +		   [initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
    4.13  		   I));
    4.14  
    4.15  
     5.1 --- a/src/Provers/classical.ML	Wed Mar 17 16:33:00 1999 +0100
     5.2 +++ b/src/Provers/classical.ML	Wed Mar 17 16:33:47 1999 +0100
     5.3 @@ -807,15 +807,15 @@
     5.4  
     5.5  val claset_ref_of_sg = Sign.get_data clasetK (fn ClasetData (ref (CSData r)) => r);
     5.6  
     5.7 -val claset_ref_of = claset_ref_of_sg o sign_of;
     5.8 +val claset_ref_of = claset_ref_of_sg o Theory.sign_of;
     5.9  val claset_of_sg = ! o claset_ref_of_sg;
    5.10 -val claset_of = claset_of_sg o sign_of;
    5.11 +val claset_of = claset_of_sg o Theory.sign_of;
    5.12  
    5.13 -fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state;
    5.14 -fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state;
    5.15 +fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
    5.16 +fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
    5.17  
    5.18  val claset = claset_of o Context.the_context;
    5.19 -val claset_ref = claset_ref_of_sg o sign_of o Context.the_context;
    5.20 +val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
    5.21  
    5.22  
    5.23  (* change claset *)
     6.1 --- a/src/Provers/simplifier.ML	Wed Mar 17 16:33:00 1999 +0100
     6.2 +++ b/src/Provers/simplifier.ML	Wed Mar 17 16:33:47 1999 +0100
     6.3 @@ -280,13 +280,13 @@
     6.4  (* access global simpset *)
     6.5  
     6.6  val simpset_of_sg = ! o simpset_ref_of_sg;
     6.7 -val simpset_of = simpset_of_sg o sign_of;
     6.8 +val simpset_of = simpset_of_sg o Theory.sign_of;
     6.9  
    6.10 -fun SIMPSET tacf state = tacf (simpset_of_sg (sign_of_thm state)) state;
    6.11 -fun SIMPSET' tacf i state = tacf (simpset_of_sg (sign_of_thm state)) i state;
    6.12 +fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
    6.13 +fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
    6.14  
    6.15  val simpset = simpset_of o Context.the_context;
    6.16 -val simpset_ref = simpset_ref_of_sg o sign_of o Context.the_context;
    6.17 +val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
    6.18  
    6.19  
    6.20  (* change global simpset *)