diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Unification.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -461,7 +461,7 @@
     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