src/HOL/Tools/datatype_package.ML

 (** Isar tactic emulations **)
 
 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))));
 
 val inst_tac = Method.bires_inst_tac false;