src/HOL/ex/Unification.thy

   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   have "unify_dom (M, M')"
     by (rule acc_downward) (rule unify_rel.intros)
   hence no_new_vars: 
     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
-    by (rule unify_vars)
+    by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
 
   from ih2 show ?case 
   proof 
     assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
     then obtain v