src/HOL/Tools/meson.ML

                          (has_fewer_prems 1, sizef)
                          (prolog_step_tac (make_horns cls) 1));
 
 (*First, breaks the goal into independent units*)
 val safe_best_meson_tac =
-     SELECT_GOAL (TRY Safe_tac THEN
+     SELECT_GOAL (TRY (CLASET safe_tac) THEN
                   TRYALL (best_meson_tac size_of_subgoals));
 
 (** Depth-first search version **)
 
 val depth_meson_tac =