# HG changeset patch
# User wenzelm
# Date 971215402 -7200
# Node ID c452fea3ce747cc69859eb6d828cb53c3cf5b053
# Parent  4a7a1091cf6561f0973a3b9b7897f09d9c27cbb2
fixed 'clarify': CHANGED;

diff -r 4a7a1091cf65 -r c452fea3ce74 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Oct 10 23:44:44 2000 +0200
+++ b/src/Provers/classical.ML	Wed Oct 11 00:03:22 2000 +0200
@@ -1174,7 +1174,7 @@
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
   ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
-  ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
+  ("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"),
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),