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