theory Data_slot
imports Main
begin

ML {*
  fun ML_exec prog = ML_Compiler.eval true Position.none
                        (ML_Lex.tokenize prog)

  fun prog_data_slot name tp empty  = 
  "structure " ^ name ^ " = Theory_Data ( " ^
  "type T = "^ tp ^" " ^
  "val empty = " ^ empty ^ " ; "^
  "val extend = I; "^
  "fun merge (x, y) = x) "^
  "fun "^ name ^ "_store v =  Context.>>(Context.map_theory (" ^ name ^".map (fn x => v))) "^
  "fun "^ name ^ "_get () = Context.>>>(Context.map_theory_result (fn th => "^
  "                                     ("^ name ^".get th, th))) "

  fun data_slot name tp empty  = ML_exec (prog_data_slot name tp empty)
  val empty_term = @{term "x"}
  val empty_cterm = @{cterm "x"}
  val empty_thm = @{thm ext}
*}

end