src/HOL/Subst/Unify.thy

--- a/src/HOL/Subst/Unify.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Subst/Unify.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
 header {* Unification Algorithm *}
 
 theory Unify
-imports Unifier
+imports Unifier "~~/src/HOL/Library/Old_Recdef"
 begin
 
 subsection {* Substitution and Unification in Higher-Order Logic. *}