diff -r 8c1dfd6c2262 -r 5cfc1c36ae97 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 theory Ferrack
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 uses ("ferrack_tac.ML")
 begin