theory Scratch
  imports Main
  keywords "letfact" :: prf_decl % "proof"
begin

ML \<open>
fun letfact_cmd (pat,(fact,_)) ctxt = 
  let val t = Proof_Context.get_fact_single ctxt fact |> Thm.prop_of
      val pat_term = Syntax.read_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) pat
      val ctxt' = Proof_Context.match_bind true [([pat_term],t)] ctxt |> snd
  in ctxt' end
val _ =
  Outer_Syntax.command \<^command_keyword>\<open>letfact\<close> "bind a fact to a schematic variable"
    ( (Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.thm))
      >> (Toplevel.proof o Proof.map_context o letfact_cmd))
\<close>


lemma "length l \<ge> 1"
proof (cases l)
  case Nil
  then show ?thesis sorry
next
  case (Cons a list)
  letfact "_ = ?rhs" = Cons
  term ?rhs
  oops

end