src/HOL/ex/Unification.thy
changeset 23373 ead82c82da9e
parent 23219 87ad6e8a5f2c
child 23777 60b7800338d5
     1.1 --- a/src/HOL/ex/Unification.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -461,7 +461,7 @@
     1.4      by (rule acc_downward) (rule unify_rel.intros)
     1.5    hence no_new_vars: 
     1.6      "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
     1.7 -    by (rule unify_vars)
     1.8 +    by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
     1.9  
    1.10    from ih2 show ?case 
    1.11    proof