src/Pure/Isar/args.ML
changeset 18728 6790126ab5f6
parent 18635 58bbff56a914
child 18998 10c251f29847
     1.1 --- a/src/Pure/Isar/args.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  signature ARGS =
     1.6  sig
     1.7 -  datatype value = Name of string | Typ of typ | Term of term | Fact of thm list |
     1.8 -    Attribute of Context.generic attribute
     1.9 +  datatype value =
    1.10 +    Name of string | Typ of typ | Term of term | Fact of thm list | Attribute of attribute
    1.11    type T
    1.12    val string_of: T -> string
    1.13    val mk_ident: string * Position.T -> T
    1.14 @@ -20,7 +20,7 @@
    1.15    val mk_typ: typ -> T
    1.16    val mk_term: term -> T
    1.17    val mk_fact: thm list -> T
    1.18 -  val mk_attribute: Context.generic attribute -> T
    1.19 +  val mk_attribute: attribute -> T
    1.20    val stopper: T * (T -> bool)
    1.21    val not_eof: T -> bool
    1.22    type src
    1.23 @@ -64,7 +64,7 @@
    1.24    val internal_typ: T list -> typ * T list
    1.25    val internal_term: T list -> term * T list
    1.26    val internal_fact: T list -> thm list * T list
    1.27 -  val internal_attribute: T list -> Context.generic attribute * T list
    1.28 +  val internal_attribute: T list -> attribute * T list
    1.29    val named_name: (string -> string) -> T list -> string * T list
    1.30    val named_typ: (string -> typ) -> T list -> typ * T list
    1.31    val named_term: (string -> term) -> T list -> term * T list
    1.32 @@ -118,7 +118,7 @@
    1.33    Typ of typ |
    1.34    Term of term |
    1.35    Fact of thm list |
    1.36 -  Attribute of Context.generic attribute;
    1.37 +  Attribute of attribute;
    1.38  
    1.39  datatype slot =
    1.40    Empty |