# HG changeset patch
# User wenzelm
# Date 1303469208 -7200
# Node ID cd5005020f4efe76e7d8eb1bd92bdc5848704620
# Parent  f7f796ce5d68bad285536490701520ba2665cad5
clarified simpset setup;
discontinued unused old-style FOL_css;

diff -r f7f796ce5d68 -r cd5005020f4e src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Apr 22 00:57:59 2011 +0200
+++ b/src/FOL/FOL.thy	Fri Apr 22 12:46:48 2011 +0200
@@ -122,7 +122,7 @@
 
 (*** Tactics for implication and contradiction ***)
 
-(*Classical <-> elimination.  Proof substitutes P=Q in 
+(*Classical <-> elimination.  Proof substitutes P=Q in
     ~P ==> ~Q    and    P ==> Q  *)
 lemma iffCE:
   assumes major: "P<->Q"
@@ -305,7 +305,19 @@
 
 
 use "simpdata.ML"
-setup simpsetup
+ML {*
+(*intuitionistic simprules only*)
+val IFOL_ss =
+  FOL_basic_ss
+  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
+  addsimprocs [defALL_regroup, defEX_regroup]
+  addcongs [@{thm imp_cong}];
+
+(*classical simprules too*)
+val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
+*}
+
+setup {* Simplifier.map_simpset (K FOL_ss) *}
 setup "Simplifier.method_setup Splitter.split_modifiers"
 setup Splitter.setup
 setup clasimp_setup
diff -r f7f796ce5d68 -r cd5005020f4e src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 22 00:57:59 2011 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 22 12:46:48 2011 +0200
@@ -136,19 +136,6 @@
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 
-(*intuitionistic simprules only*)
-val IFOL_ss =
-  FOL_basic_ss
-  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
-  addsimprocs [defALL_regroup, defEX_regroup]    
-  addcongs [@{thm imp_cong}];
-
-(*classical simprules too*)
-val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
-
-val simpsetup = Simplifier.map_simpset (K FOL_ss);
-
-
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun
@@ -160,4 +147,3 @@
 ML_Antiquote.value "clasimpset"
   (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
 
-val FOL_css = (FOL_cs, FOL_ss);
diff -r f7f796ce5d68 -r cd5005020f4e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 22 00:57:59 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 22 12:46:48 2011 +0200
@@ -1209,10 +1209,12 @@
 
 use "Tools/simpdata.ML"
 ML {* open Simpdata *}
+setup {*
+  Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
+*}
 
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
-  #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
   #> Splitter.setup
   #> clasimp_setup
   #> EqSubst.setup
diff -r f7f796ce5d68 -r cd5005020f4e src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 00:57:59 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 12:46:48 2011 +0200
@@ -191,9 +191,6 @@
   Simplifier.simproc_global @{theory}
     "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
 
-
-val simpset_simprocs = HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]
-
 end;
 
 structure Splitter = Simpdata.Splitter;