# HG changeset patch
# User wenzelm
# Date 953142003 -3600
# Node ID 482c301041b495982784fdfe4b9679c3426cd3de
# Parent  d99902232df8e1ce42bee017172411690e8868d4
include Splitter.split_modifiers;

diff -r d99902232df8 -r 482c301041b4 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Mar 15 18:38:52 2000 +0100
+++ b/src/Provers/clasimp.ML	Wed Mar 15 18:40:03 2000 +0100
@@ -3,7 +3,7 @@
     Author:     David von Oheimb, TU Muenchen
 
 Combination of classical reasoner and simplifier (depends on
-simplifier.ML, classical.ML, blast.ML).
+simplifier.ML, splitter.ML classical.ML, blast.ML).
 *)
 
 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2;
@@ -12,6 +12,7 @@
 signature CLASIMP_DATA =
 sig
   structure Simplifier: SIMPLIFIER
+  structure Splitter: SPLITTER
   structure Classical: CLASSICAL
   structure Blast: BLAST
   sharing type Classical.claset = Blast.claset
@@ -152,7 +153,8 @@
 fun get_local_clasimpset ctxt =
   (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
 
-val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
+val clasimp_modifiers =
+  Simplifier.simp_modifiers @ Splitter.split_modifiers @ Classical.cla_modifiers;
 
 fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));