clarsimp_tac now copes with the (unwanted) case that the simplifier splits
the goal
--- a/src/Provers/clasimp.ML Wed Oct 27 18:12:40 1999 +0200
+++ b/src/Provers/clasimp.ML Wed Oct 27 19:29:47 1999 +0200
@@ -90,7 +90,7 @@
Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
-fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_MAYBE'
+fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_ALL_NEW
Classical.clarify_tac (cs addSss ss);
fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;