src/FOL/simpdata.ML
changeset 7355 4c43090659ca
parent 6391 0da748358eff
child 7570 a9391550eea1
     1.1 --- a/src/FOL/simpdata.ML	Wed Aug 25 20:42:01 1999 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Aug 25 20:45:19 1999 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  fun prove_fun s = 
     1.6   (writeln s;  
     1.7 -  prove_goal FOL.thy s
     1.8 +  prove_goal (the_context ()) s
     1.9     (fn prems => [ (cut_facts_tac prems 1), 
    1.10                    (Cla.fast_tac FOL_cs 1) ]));
    1.11  
    1.12 @@ -177,7 +177,7 @@
    1.13      (fn prems => [ (cut_facts_tac prems 1), 
    1.14                     (IntPr.fast_tac 1) ]);
    1.15  
    1.16 -fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
    1.17 +fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]);
    1.18  
    1.19  int_prove "conj_commute" "P&Q <-> Q&P";
    1.20  int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
    1.21 @@ -242,11 +242,12 @@
    1.22  end);
    1.23  
    1.24  local
    1.25 +
    1.26  val ex_pattern =
    1.27 -  read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
    1.28 +  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
    1.29  
    1.30  val all_pattern =
    1.31 -  read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.32 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.33  
    1.34  in
    1.35  val defEX_regroup =
    1.36 @@ -348,8 +349,7 @@
    1.37  (*classical simprules too*)
    1.38  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
    1.39  
    1.40 -simpset_ref() := FOL_ss;
    1.41 -
    1.42 +val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
    1.43  
    1.44  
    1.45  (*** integration of simplifier with classical reasoner ***)