1.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:52:46 2008 +0200
     1.3 @@ -215,10 +215,10 @@
     1.4  
     1.5  (* tags *)
     1.6  
     1.7 -val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
     1.8 -val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
     1.9 +val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
    1.10 +val untagged = syntax (Scan.lift Args.name >> Thm.untag);
    1.11  
    1.12 -val kind = syntax (Scan.lift Args.name >> PureThy.kind);
    1.13 +val kind = syntax (Scan.lift Args.name >> Thm.kind);
    1.14  
    1.15  
    1.16  (* rule composition *)