--- a/src/HOL/Coinduction.thy Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Coinduction.thy Thu Nov 21 21:33:34 2013 +0100
@@ -9,7 +9,7 @@
header {* Coinduction Method *}
theory Coinduction
-imports Inductive
+imports Ctr_Sugar
begin
ML_file "Tools/coinduction.ML"