| changeset 26806 | 40b411ec05aa |
| parent 24823 | bfb619994060 |
| child 38140 | 05691ad74079 |
--- a/src/HOL/Subst/Unify.thy Wed May 07 10:56:58 2008 +0200 +++ b/src/HOL/Subst/Unify.thy Wed May 07 10:57:19 2008 +0200 @@ -117,7 +117,7 @@ apply blast txt{*@{text finite_psubset} case*} apply (simp add: unifyRel_def lex_prod_def) -apply (simp add: finite_psubset_def finite_vars_of psubset_def) +apply (simp add: finite_psubset_def finite_vars_of psubset_eq) apply blast txt{*Final case, also @{text finite_psubset}*} apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)