src/HOL/Subst/Unify.ML
changeset 3724 f33e301a89f5
parent 3392 d0d86b96aa96
child 3919 c036caebfc75
     1.1 --- a/src/HOL/Subst/Unify.ML	Mon Sep 29 11:36:44 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Mon Sep 29 11:37:02 1997 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
     1.5  				 wf_measure]) 1);
     1.6  (* TC *)
     1.7 -by (Step_tac 1);
     1.8 +by Safe_tac;
     1.9  by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.10  				 lex_prod_def, measure_def, inv_image_def]) 1);
    1.11  by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);