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