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);