--- a/src/HOL/Tools/Meson/meson.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri May 13 22:55:00 2011 +0200
@@ -699,8 +699,7 @@
(*First, breaks the goal into independent units*)
fun safe_best_meson_tac ctxt =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
- TRYALL (best_meson_tac size_of_subgoals ctxt));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
(** Depth-first search version **)
@@ -742,7 +741,7 @@
end));
fun meson_tac ctxt ths =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
(**** Code to support ordinary resolution, rather than Model Elimination ****)