diff -r 2c69bb1374b8 -r 688a8a7bcd4e src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jul 19 21:47:39 2007 +0200
@@ -5,7 +5,7 @@
 header {* Quatifier elimination for R(0,1,+,<) *}
 
 theory ReflectedFerrack
-  imports GCD Real EfficientNat
+  imports GCD Real Efficient_Nat
   uses ("linreif.ML") ("linrtac.ML")
 begin