14   Every generic data slot may keep data of any kind which is stored in the

    14   Every generic data slot may keep data of any kind which is stored in the

    15   context.

    15   context.

    16 

    16 

    17   *}

    17   *}

    18 

    18 

    21 

    20 

    22 structure Data = GenericDataFun

    21 structure Data = GenericDataFun

    23  ( type T = int Symtab.table

    22  ( type T = int Symtab.table

    24    val empty = Symtab.empty

    23    val empty = Symtab.empty

    25    val extend = I

    24    val extend = I

    26    fun merge _ = Symtab.merge (K true)

    25    fun merge _ = Symtab.merge (K true)

    27  )

    26  )

    28 

    27 

    29 in

    28 in

    35 end *}

    31 end *}

    36 

    32 

    37 setup {* Context.theory_map (update "foo" 1) *}

    33 setup {* Context.theory_map (update "foo" 1) *}

    38 

    34 

    39 text {*

    35 text {*