# HG changeset patch
# User wenzelm
# Date 1004133950 -7200
# Node ID 2ece34b9fd8e36d8caf7e7787e0e1af517cd5a16
# Parent  f1657e0291cad1e070d4d3aade7d63c4d77d90c9
Isar: fixed rep_datatype args;

diff -r f1657e0291ca -r 2ece34b9fd8e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Oct 27 00:05:14 2001 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 27 00:05:50 2001 +0200
@@ -766,6 +766,7 @@
 val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i;
 
 
+
 (******************************** add datatype ********************************)
 
 fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
@@ -870,8 +871,8 @@
 
 val rep_datatype_decl =
   Scan.option (Scan.repeat1 P.name) --
-    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [] --
-    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [] --
+    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
+    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
     (P.$$$ "induction" |-- P.!!! P.xthm);
 
 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #1 o rep_datatype opt_ts dss iss ind;