theory Generic
imports Main
keywords
  "test_thy" :: thy_decl and
  "test_prf" :: thy_decl
begin

ML {*
structure Data = Generic_Data
  (type T = string
   val empty = ""
   val extend = I
   val merge = fst)

fun test_thy_cmd name =
  Context.Proof #> Data.put name #> Context.proof_of


val () = Outer_Syntax.local_theory @{command_spec "test_thy"}
  "test" (Parse.name >> test_thy_cmd)
*}

test_thy foo

ML_val {* Data.get (Context.Theory @{theory}) *}
ML_val {* Data.get (Context.Proof @{context}) *}

ML {*
fun test_prf_cmd name =
  Local_Theory.background_theory (Context.Theory #> Data.put name #> Context.theory_of)

val () = Outer_Syntax.local_theory @{command_spec "test_prf"}
  "test" (Parse.name >> test_prf_cmd)
*}

test_prf bar

ML_val {* Data.get (Context.Theory @{theory}) *}
ML_val {* Data.get (Context.Proof @{context}) *}

end