type/const name: explicitly allow abbreviations as well;
authorwenzelm
Sat Feb 27 20:55:18 2010 +0100 (2010-02-27)
changeset 354001fad91c02b98
parent 35399 3881972fcfca
child 35401 bfcbab8592ba
type/const name: explicitly allow abbreviations as well;
src/Tools/induct.ML
     1.1 --- a/src/Tools/induct.ML	Sat Feb 27 20:51:51 2010 +0100
     1.2 +++ b/src/Tools/induct.ML	Sat Feb 27 20:55:18 2010 +0100
     1.3 @@ -345,9 +345,9 @@
     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 true) >> add_type ||
     1.8 -  spec predN Args.const >> add_pred ||
     1.9 -  spec setN Args.const >> add_pred ||
    1.10 +  spec typeN (Args.type_name false) >> add_type ||
    1.11 +  spec predN (Args.const false) >> add_pred ||
    1.12 +  spec setN (Args.const false) >> add_pred ||
    1.13    Scan.lift Args.del >> K del;
    1.14  
    1.15  in
    1.16 @@ -856,9 +856,9 @@
    1.17        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
    1.18  
    1.19  fun rule get_type get_pred =
    1.20 -  named_rule typeN (Args.type_name true) get_type ||
    1.21 -  named_rule predN Args.const get_pred ||
    1.22 -  named_rule setN Args.const get_pred ||
    1.23 +  named_rule typeN (Args.type_name false) get_type ||
    1.24 +  named_rule predN (Args.const false) get_pred ||
    1.25 +  named_rule setN (Args.const false) get_pred ||
    1.26    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
    1.27  
    1.28  val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;