allow empty set/type name;
authorwenzelm
Tue Oct 16 00:32:34 2001 +0200 (2001-10-16)
changeset 117912c201f3b018e
parent 11790 42393a11642d
child 11792 311eee3d63b6
allow empty set/type name;
src/Pure/Isar/induct_attrib.ML
     1.1 --- a/src/Pure/Isar/induct_attrib.ML	Tue Oct 16 00:32:01 2001 +0200
     1.2 +++ b/src/Pure/Isar/induct_attrib.ML	Tue Oct 16 00:32:34 2001 +0200
     1.3 @@ -202,12 +202,14 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
     1.8 +fun spec k cert =
     1.9 +  (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
    1.10 +  Args.$$$ k >> K "";
    1.11  
    1.12  fun attrib sign_of add_type add_set = Scan.depend (fn x =>
    1.13    let val sg = sign_of x in
    1.14 -    spec typeN >> (add_type o Sign.certify_tyname sg o Sign.intern_tycon sg) ||
    1.15 -    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
    1.16 +    spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
    1.17 +    spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
    1.18    end >> pair x);
    1.19  
    1.20  in