diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -215,10 +215,10 @@
 
 (* tags *)
 
-val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
-val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
+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 >> PureThy.kind);
+val kind = syntax (Scan.lift Args.name >> Thm.kind);
 
 
 (* rule composition *)