--- a/src/HOL/ex/meson.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/meson.ML Wed Nov 05 13:23:46 1997 +0100
@@ -430,7 +430,7 @@
(*First, breaks the goal into independent units*)
val safe_best_meson_tac =
- SELECT_GOAL (TRY (safe_tac (claset())) THEN
+ SELECT_GOAL (TRY Safe_tac THEN
TRYALL (best_meson_tac size_of_subgoals));
(** Depth-first search version **)
@@ -464,7 +464,7 @@
(prolog_step_tac' (make_horns cls))));
val safe_meson_tac =
- SELECT_GOAL (TRY (safe_tac (claset())) THEN
+ SELECT_GOAL (TRY Safe_tac THEN
TRYALL (iter_deepen_meson_tac));