src/HOL/ex/Unification.thy
changeset 23777 60b7800338d5
parent 23373 ead82c82da9e
child 24444 448978b61556
     1.1 --- a/src/HOL/ex/Unification.thy	Wed Jul 11 11:52:45 2007 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Wed Jul 11 11:54:03 2007 +0200
     1.3 @@ -458,7 +458,7 @@
     1.4  
     1.5    from `unify_dom (M \<cdot> N, M' \<cdot> N')`
     1.6    have "unify_dom (M, M')"
     1.7 -    by (rule acc_downward) (rule unify_rel.intros)
     1.8 +    by (rule accp_downward) (rule unify_rel.intros)
     1.9    hence no_new_vars: 
    1.10      "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
    1.11      by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)