src/FOL/simpdata.ML

 
 (*** Classical laws ***)
 
 fun prove_fun s = 
  (writeln s;  
-  prove_goal FOL.thy s
+  prove_goal (the_context ()) s
    (fn prems => [ (cut_facts_tac prems 1), 
                   (Cla.fast_tac FOL_cs 1) ]));
 
 (*Avoids duplication of subgoals after expand_if, when the true and false 
   cases boil down to the same thing.*) 

 
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
                    (IntPr.fast_tac 1) ]);
 
-fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
+fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]);
 
 int_prove "conj_commute" "P&Q <-> Q&P";
 int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
 val conj_comms = [conj_commute, conj_left_commute];
 

   val allI = allI
   val allE = allE
 end);
 
 local
+
 val ex_pattern =
-  read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
+  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
 
 val all_pattern =
-  read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
+  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
 
 in
 val defEX_regroup =
   mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
 val defALL_regroup =

       "(~P <-> ~Q) <-> (P<->Q)"];
 
 (*classical simprules too*)
 val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
 
-simpset_ref() := FOL_ss;
-
+val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
 
 
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun