src/Provers/clasimp.ML

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