src/HOL/ex/meson.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4271 3a82492e70c5
     1.1 --- a/src/HOL/ex/meson.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/ex/meson.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -430,7 +430,7 @@
     1.4  
     1.5  (*First, breaks the goal into independent units*)
     1.6  val safe_best_meson_tac =
     1.7 -     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
     1.8 +     SELECT_GOAL (TRY Safe_tac THEN 
     1.9                    TRYALL (best_meson_tac size_of_subgoals));
    1.10  
    1.11  (** Depth-first search version **)
    1.12 @@ -464,7 +464,7 @@
    1.13                             (prolog_step_tac' (make_horns cls))));
    1.14  
    1.15  val safe_meson_tac =
    1.16 -     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
    1.17 +     SELECT_GOAL (TRY Safe_tac THEN 
    1.18                    TRYALL (iter_deepen_meson_tac));
    1.19  
    1.20