1249   associated data. This is different for theories, where the command 

  1249   associated data. This is different for theories, where the command 

  1250   \isacommand{setup} registers the data with the current and future 

  1250   \isacommand{setup} registers the data with the current and future 

  1251   theories, and therefore one can access the data potentially 

  1251   theories, and therefore one can access the data potentially 

  1252   indefinitely.

  1252   indefinitely.

  1253 

  1253 

  1254   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 

  1256   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 

  1255   for treating theories and proof contexts more uniformly. This type is defined as follows

  1257   for treating theories and proof contexts more uniformly. This type is defined as follows

  1256 *}

  1258 *}

  1257 

  1259 

  1258 ML_val{*datatype generic = 

  1260 ML_val{*datatype generic =