| changeset 18799 | f137c5e971f5 |
| parent 18734 | f5ea6b0d3501 |
| child 18821 | 213b7341abb6 |
--- a/src/Pure/Isar/attrib.ML Fri Jan 27 18:29:33 2006 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Jan 27 19:03:02 2006 +0100 @@ -202,8 +202,8 @@ (* tags *) -fun tagged x = syntax (tag >> Drule.tag) x; -fun untagged x = syntax (Scan.lift Args.name >> Drule.untag) x; +fun tagged x = syntax (tag >> PureThy.tag) x; +fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x; (* rule composition *)