| changeset 18988 | d6e5fa2ba8b8 |
| parent 18964 | 67f572e03236 |
| child 19008 | 14c1b2f5dda4 |
--- a/src/HOL/Tools/datatype_package.ML Fri Feb 10 02:22:13 2006 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Feb 10 02:22:16 2006 +0100 @@ -262,7 +262,7 @@ local val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); -val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm); +val opt_rule = Scan.option (rule_spec |-- Attrib.thm); val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));