src/Pure/Isar/attrib.ML

 (** Pure attributes **)
 
 (* tags *)
 
 fun gen_tag x = syntax (tag >> Drule.tag) x;
-fun gen_untag x = syntax (tag >> Drule.untag) x;
+fun gen_untag x = syntax (Scan.lift Args.name >> Drule.untag) x;
 
 
 (* transfer *)
 
 fun gen_transfer theory_of = no_args (Drule.rule_attribute (fn st => Thm.transfer (theory_of st)));