--- a/src/HOL/Tools/coinduction.ML Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML Thu Mar 06 13:44:01 2014 +0100
@@ -130,8 +130,8 @@
fun rule get_type get_pred =
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 ||
+ named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
+ named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;