theory Scratch
  imports Main
begin

locale test
begin

local_setup \<open>fn lthy =>
  let
    val (res', lthy') = lthy
      |> Local_Theory.abbrev Syntax.mode_default ((@{binding a}, NoSyn), @{term Nil});
    val res = res' |> apply2 (Morphism.term (Proof_Context.export_morphism lthy lthy'));
    val result = res' |> apply2 (Morphism.term (Local_Theory.target_morphism lthy'));
    val _ = @{print tracing} {res' = res', res = res, result = result};

    (*experiments with Syntax.read_term -- it is UNUSUAL to invoke
      that in the middle of a definitional package!*)
    val t = Syntax.read_term lthy' "a";
    val t' = Syntax.read_term (Local_Theory.target_of lthy') "a";

    (*expand according to Local_Defs.fixed_abbrevs*)
    val expand = Envir.expand_term_frees [(dest_Free (#1 res'), #2 res')];
    val _ = @{print tracing} {t = t, t' = t', t_expanded = expand t};
  in lthy' end;
\<close>

end

end