src/Pure/Isar/attrib.ML

   syntax (Scan.lift Args.internal_attribute >> Morphism.form);
 
 
 (* tags *)
 
-val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
-val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
-
-val kind = syntax (Scan.lift Args.name >> PureThy.kind);
+val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
+val untagged = syntax (Scan.lift Args.name >> Thm.untag);
+
+val kind = syntax (Scan.lift Args.name >> Thm.kind);
 
 
 (* rule composition *)
 
 val COMP_att =