theory Test
imports Pure
keywords "def_id" :: thy_decl
begin

named_theorems rules

ML ‹
Outer_Syntax.local_theory \<^command_keyword>‹def_id› ""
  (Scan.succeed (fn lthy =>
    let
      val ((_, (_, th)), lthy') =
        Local_Theory.define (
          (Binding.qualified_name "id", NoSyn),
          ((Binding.qualified_name "id_def", []), @{term "λx. x"})
        ) lthy
    in
      tracing (@{make_string} th);
      lthy' |> Context.proof_map (Named_Theorems.add_thm
\<^named_theorems>‹rules› th)
    end))
›

(* prints "id == λx. x" *)
def_id

(* these are fine *)
term id
thm id_def

(* EMPTY! *)
thm rules

end