src/Provers/classical.ML

 val setup_methods = Method.add_methods
  [("single", Method.no_args single, "apply standard rule (single step)"),
   ("default", Method.no_args single, "apply standard rule (single step)"),
   ("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"),
+  ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac"),
+  ("step_tac", cla_method' step_tac, "step_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)")];