--- a/src/Tools/induct.ML Thu Mar 06 17:55:39 2014 +0100
+++ b/src/Tools/induct.ML Thu Mar 06 22:15:01 2014 +0100
@@ -361,9 +361,9 @@
Scan.lift (Args.$$$ k) >> K "";
fun attrib add_type add_pred del =
- spec typeN (Args.type_name false) >> add_type ||
- spec predN (Args.const false) >> add_pred ||
- spec setN (Args.const false) >> add_pred ||
+ spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
+ spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
+ spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
Scan.lift Args.del >> K del;
in
@@ -883,9 +883,9 @@
| NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
fun rule get_type get_pred =
- named_rule typeN (Args.type_name false) get_type ||
- named_rule predN (Args.const false) get_pred ||
- named_rule setN (Args.const false) get_pred ||
+ named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
+ named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
+ named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;