src/Pure/defs.ML
changeset 17711 c16cbe73798c
parent 17707 bc0270e9d27f
child 17712 46c2091e5187
equal deleted inserted replaced
17710:9a13e0abdb82 17711:c16cbe73798c
    13   val define: string -> string * typ -> (string * typ) list -> T -> T
    13   val define: string -> string * typ -> (string * typ) list -> T -> T
    14   val empty: T
    14   val empty: T
    15   val merge: Pretty.pp -> T * T -> T
    15   val merge: Pretty.pp -> T * T -> T
    16 end
    16 end
    17 
    17 
    18 structure Defs (* FIXME : DEFS *) =
    18 structure Defs: DEFS =
    19 struct
    19 struct
    20 
    20 
    21 (** datatype T **)
    21 (** datatype T **)
    22 
    22 
    23 datatype T = Defs of
    23 datatype T = Defs of