Isar: fixed rep_datatype args;
authorwenzelm
Sat Oct 27 00:05:50 2001 +0200 (2001-10-27)
changeset 119582ece34b9fd8e
parent 11957 f1657e0291ca
child 11959 ed914e8a0fd1
Isar: fixed rep_datatype args;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Oct 27 00:05:14 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 27 00:05:50 2001 +0200
     1.3 @@ -766,6 +766,7 @@
     1.4  val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i;
     1.5  
     1.6  
     1.7 +
     1.8  (******************************** add datatype ********************************)
     1.9  
    1.10  fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
    1.11 @@ -870,8 +871,8 @@
    1.12  
    1.13  val rep_datatype_decl =
    1.14    Scan.option (Scan.repeat1 P.name) --
    1.15 -    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [] --
    1.16 -    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [] --
    1.17 +    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
    1.18 +    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
    1.19      (P.$$$ "induction" |-- P.!!! P.xthm);
    1.20  
    1.21  fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #1 o rep_datatype opt_ts dss iss ind;