src/Tools/induct.ML
changeset 55951 c07d184aebe9
parent 54742 7a86358a3c0b
child 55954 a29aefc88c8d
     1.1 --- a/src/Tools/induct.ML	Thu Mar 06 11:32:16 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Thu Mar 06 12:10:19 2014 +0100
     1.3 @@ -361,7 +361,7 @@
     1.4    Scan.lift (Args.$$$ k) >> K "";
     1.5  
     1.6  fun attrib add_type add_pred del =
     1.7 -  spec typeN (Args.type_name false) >> add_type ||
     1.8 +  spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
     1.9    spec predN (Args.const false) >> add_pred ||
    1.10    spec setN (Args.const false) >> add_pred ||
    1.11    Scan.lift Args.del >> K del;
    1.12 @@ -883,7 +883,7 @@
    1.13        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
    1.14  
    1.15  fun rule get_type get_pred =
    1.16 -  named_rule typeN (Args.type_name false) get_type ||
    1.17 +  named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
    1.18    named_rule predN (Args.const false) get_pred ||
    1.19    named_rule setN (Args.const false) get_pred ||
    1.20    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;