--- a/src/HOL/Recdef.thy Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Recdef.thy Thu Aug 19 16:03:01 2010 +0200
@@ -5,7 +5,7 @@
header {* TFL: recursive function definitions *}
theory Recdef
-imports FunDef Plain
+imports Plain Hilbert_Choice
uses
("Tools/TFL/casesplit.ML")
("Tools/TFL/utils.ML")