diff -r 000000000000 -r 1378b654acde thys/Data_slot.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Data_slot.thy	Thu Mar 06 13:28:38 2014 +0000
@@ -0,0 +1,25 @@
+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