src/HOL/Tools/datatype_package.ML
changeset 22101 6d13239d5f52
parent 21772 7c7ade4f537b
child 22480 b20bc8029edb
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:07 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:08 2007 +0100
     1.3 @@ -1030,9 +1030,9 @@
     1.4  
     1.5  val rep_datatype_decl =
     1.6    Scan.option (Scan.repeat1 P.name) --
     1.7 -    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
     1.8 -    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
     1.9 -    (P.$$$ "induction" |-- P.!!! P.xthm);
    1.10 +    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
    1.11 +    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
    1.12 +    (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
    1.13  
    1.14  fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
    1.15