# HG changeset patch
# User wenzelm
# Date 1003185154 -7200
# Node ID 2c201f3b018efb0bdd7f26aff3d9956653a0570b
# Parent  42393a11642ddafdb4e4ee9e0521c040d1d62278
allow empty set/type name;

diff -r 42393a11642d -r 2c201f3b018e src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Tue Oct 16 00:32:01 2001 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Tue Oct 16 00:32:34 2001 +0200
@@ -202,12 +202,14 @@
 
 local
 
-fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
+fun spec k cert =
+  (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
+  Args.$$$ k >> K "";
 
 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   let val sg = sign_of x in
-    spec typeN >> (add_type o Sign.certify_tyname sg o Sign.intern_tycon sg) ||
-    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
+    spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
+    spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
   end >> pair x);
 
 in