1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -699,8 +699,7 @@
     1.4  
     1.5  (*First, breaks the goal into independent units*)
     1.6  fun safe_best_meson_tac ctxt =
     1.7 -     SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
     1.8 -                  TRYALL (best_meson_tac size_of_subgoals ctxt));
     1.9 +  SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
    1.10  
    1.11  (** Depth-first search version **)
    1.12  
    1.13 @@ -742,7 +741,7 @@
    1.14          end));
    1.15  
    1.16  fun meson_tac ctxt ths =
    1.17 -  SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
    1.18 +  SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
    1.19  
    1.20  
    1.21  (**** Code to support ordinary resolution, rather than Model Elimination ****)