diff -r 19520b3d4f0d -r c799d0859638 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Jul 14 13:05:46 1999 +0200
+++ b/src/Provers/classical.ML	Wed Jul 14 13:06:08 1999 +0200
@@ -1148,12 +1148,8 @@
 
 (* contradiction *)
 
-(* FIXME
-val contradiction = Method.METHOD (fn facts =>
-  Method.FINISHED (ALLGOALS (Method.same_tac facts THEN' (contr_tac ORELSE' assume_tac))));
-*)
-
-val contradiction = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
+val contradiction =
+  Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
 
 
 (* automatic methods *)
@@ -1188,10 +1184,10 @@
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("safe_tac", cla_method safe_tac, "safe_tac"),
   ("safe_step", cla_method' safe_step_tac, "step_tac"),
-  ("fast", cla_method' fast_tac, "fast_tac"),
-  ("best", cla_method' best_tac, "best_tac"),
-  ("slow", cla_method' slow_tac, "slow_tac"),
-  ("slow_best", cla_method' slow_best_tac, "slow_best_tac")];
+  ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
+  ("best", cla_method' best_tac, "classical prover (best-first)"),
+  ("slow", cla_method' slow_tac, "classical prover (depth-first, more backtracking)"),
+  ("slow_best", cla_method' slow_best_tac, "classical prover (best-first, more backtracking)")];