clarsimp_tac now copes with the (unwanted) case that the simplifier splits
authoroheimb
Wed, 27 Oct 1999 19:29:47 +0200
changeset 7957 0196b2302e21
parent 7956 edaca60a54cd
child 7958 f531589c9fc1
clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal
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;