| changeset 8496 | 7e4a466b18d5 |
| parent 8368 | bdc3ee0d8cb6 |
| child 8633 | 427ead639d8a |
--- a/src/Pure/Isar/attrib.ML Fri Mar 17 16:27:28 2000 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Mar 17 16:28:59 2000 +0100 @@ -169,7 +169,7 @@ (* 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 *)