Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
allow empty set/type name;
authorwenzelm
Tue, 16 Oct 2001 00:32:34 +0200
changeset 11791 2c201f3b018e
parent 11790 42393a11642d
child 11792 311eee3d63b6
allow empty set/type name;
src/Pure/Isar/induct_attrib.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle