src/Pure/Isar/attrib.ML
changeset 21658 5e31241e1e3c
parent 21439 303ec9e9f74f
child 21698 43a842769765
--- 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 *)