diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -129,7 +129,7 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule Induct.typeN (Args.type_name false) get_type ||
+  named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
   named_rule Induct.predN (Args.const false) get_pred ||
   named_rule Induct.setN (Args.const false) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;