theory Generic
imports Main
keywords
  "morph" :: thy_decl and
  "morph_proof_state" :: thy_goal and
  "morph_note" :: thy_decl
begin

ML {*
structure Data = Generic_Data
  (type T = binding * thm option
   val empty = (Binding.name "", NONE)
   val extend = I
   val merge = fst)

val get_data = Data.get o Context.Proof
*}

ML {*
val opts = {pervasive=false, syntax=false}

fun test_morph_cmd name lthy =
  let
    (* We are relative to some local theory lthy here
    and have some entities (terms t, theorems thm, \<dots>) relative
    to lthy flying around as ML values here *)
    fun decl phi context =
      let
        (* We are called for each instance (interpretation)
        of the original lthy, including lthy itself; the
        logical difference is represented by morphism phi,
        which we can apply (using Morphism.\<dots>) to transform our
        original entities t, thm to obtain their appropriate
        shape to do something with them relative
        to the current instance *)
        val the_name = Binding.name name
      in Data.map (fn (old_name, thm) => (the_name, Option.map (Morphism.thm phi) thm)) context end
  in
    lthy
    |> Local_Theory.declaration opts decl
  end;

val () = Outer_Syntax.local_theory @{command_keyword "morph"}
  "test" (Parse.name >> test_morph_cmd)
*}

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

morph voila

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

ML {*
fun morph_proof_state name lthy =
  let
    fun decl thm phi context = Data.map (fn (name, old_thm) => (Morphism.binding phi name, SOME thm)) context
    fun after_qed [[thm]] ctxt = Local_Theory.declaration opts (decl thm) ctxt
      | after_qed _ _ = error "Bad"
    val prop = name ^ " = " ^ name |> Syntax.read_prop lthy
  in
    Proof.theorem NONE after_qed [[(prop, [])]] lthy
  end

val () = Outer_Syntax.local_theory_to_proof @{command_keyword "morph_proof_state"}
  "test" (Parse.name >> morph_proof_state)
*}

morph_proof_state "blargh"
  by (rule HOL.refl)

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

ML {*
fun morph_note prefix lthy =
  let
    val (name, thm) = get_data lthy
  in
    Local_Theory.note ((Binding.qualify true prefix name, []), [the thm]) lthy |> snd
  end

val () = Outer_Syntax.local_theory @{command_keyword "morph_note"}
  "test" (Parse.name >> morph_note)

*}

morph_note "exported"

thm exported.voila

end