# HG changeset patch
# User wenzelm
# Date 1267300518 -3600
# Node ID 1fad91c02b98decca5399e8ced6cb60f5dffecbd
# Parent  3881972fcfca841f8e45bfed22afe86c15d9bf9b
type/const name: explicitly allow abbreviations as well;

diff -r 3881972fcfca -r 1fad91c02b98 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Feb 27 20:51:51 2010 +0100
+++ b/src/Tools/induct.ML	Sat Feb 27 20:55:18 2010 +0100
@@ -345,9 +345,9 @@
   Scan.lift (Args.$$$ k) >> K "";
 
 fun attrib add_type add_pred del =
-  spec typeN (Args.type_name true) >> add_type ||
-  spec predN Args.const >> add_pred ||
-  spec setN Args.const >> add_pred ||
+  spec typeN (Args.type_name false) >> add_type ||
+  spec predN (Args.const false) >> add_pred ||
+  spec setN (Args.const false) >> add_pred ||
   Scan.lift Args.del >> K del;
 
 in
@@ -856,9 +856,9 @@
       | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_pred =
-  named_rule typeN (Args.type_name true) get_type ||
-  named_rule predN Args.const get_pred ||
-  named_rule setN Args.const 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 ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;