diff -r 2677db44c795 -r 727ef1b8b3ee src/HOL/Tools/datatype_package.ML
--- 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;