src/HOL/Tools/datatype_package.ML
changeset 15703 727ef1b8b3ee
parent 15661 9ef583b08647
child 15704 93163972dbdc
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -51,8 +51,8 @@
     1.4         induction : thm,
     1.5         size : thm list,
     1.6         simps : thm list}
     1.7 -  val rep_datatype : string list option -> (thmref * Args.src list) list list ->
     1.8 -    (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
     1.9 +  val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
    1.10 +    (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
    1.11        {distinct : thm list list,
    1.12         inject : thm list list,
    1.13         exhaustion : thm list,
    1.14 @@ -244,7 +244,8 @@
    1.15  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
    1.16  val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
    1.17  
    1.18 -val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
    1.19 +val varss =
    1.20 +  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
    1.21  
    1.22  val inst_tac = Method.bires_inst_tac false;
    1.23