--- a/src/FOL/FOL.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/FOL/FOL.thy Thu Apr 18 17:07:01 2013 +0200
@@ -331,16 +331,20 @@
ML {*
(*intuitionistic simprules only*)
val IFOL_ss =
- FOL_basic_ss
+ put_simpset FOL_basic_ss @{context}
addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
- |> Simplifier.add_cong @{thm imp_cong};
+ |> Simplifier.add_cong @{thm imp_cong}
+ |> simpset_of;
(*classical simprules too*)
-val FOL_ss = IFOL_ss addsimps @{thms cla_simps cla_ex_simps cla_all_simps};
+val FOL_ss =
+ put_simpset IFOL_ss @{context}
+ addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
+ |> simpset_of;
*}
-setup {* Simplifier.map_simpset_global (K FOL_ss) *}
+setup {* map_theory_simpset (put_simpset FOL_ss) *}
setup "Simplifier.method_setup Splitter.split_modifiers"
setup Splitter.setup