--- a/src/HOL/Tools/datatype_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -51,8 +51,8 @@
induction : thm,
size : thm list,
simps : thm list}
- val rep_datatype : string list option -> (thmref * Args.src list) list list ->
- (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
+ val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
+ (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -244,7 +244,8 @@
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
-val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
+val varss =
+ Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
val inst_tac = Method.bires_inst_tac false;