src/Pure/Isar/attrib.ML
changeset 21658 5e31241e1e3c
parent 21439 303ec9e9f74f
child 21698 43a842769765
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:41 2006 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Dec 05 22:14:42 2006 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4      attribute * (Context.generic * Args.T list)) -> src -> attribute
     1.5    val no_args: attribute -> src -> attribute
     1.6    val add_del_args: attribute -> attribute -> src -> attribute
     1.7 -  val internal: attribute -> src
     1.8 +  val internal: (morphism -> attribute) -> src
     1.9  end;
    1.10  
    1.11  structure Attrib: ATTRIB =
    1.12 @@ -267,7 +267,8 @@
    1.13  
    1.14  fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
    1.15  
    1.16 -fun internal_att x = syntax (Scan.lift Args.internal_attribute) x;
    1.17 +fun internal_att x =
    1.18 +  syntax (Scan.lift Args.internal_attribute >> (fn att => att Morphism.identity)) x;
    1.19  
    1.20  
    1.21  (* theory setup *)