--- a/src/Pure/Isar/attrib.ML Tue Dec 05 22:14:41 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Dec 05 22:14:42 2006 +0100
@@ -35,7 +35,7 @@
attribute * (Context.generic * Args.T list)) -> src -> attribute
val no_args: attribute -> src -> attribute
val add_del_args: attribute -> attribute -> src -> attribute
- val internal: attribute -> src
+ val internal: (morphism -> attribute) -> src
end;
structure Attrib: ATTRIB =
@@ -267,7 +267,8 @@
fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
-fun internal_att x = syntax (Scan.lift Args.internal_attribute) x;
+fun internal_att x =
+ syntax (Scan.lift Args.internal_attribute >> (fn att => att Morphism.identity)) x;
(* theory setup *)