theory Prove
imports Plain 
begin

ML {*
val r = Unsynchronized.ref (NONE:(unit -> term) option)
*}

ML {*
let
  fun after_qed thm_name thms lthy =
    Local_Theory.note (thm_name, (flat thms)) lthy |> snd
  fun setup_proof (name_spec, (txt, _)) lthy =
  let
    val trm = ML_Context.evaluate lthy true ("r", r) txt
  in
    Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
  end

  val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
in
  Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" 
    Keyword.thy_goal (parser >> setup_proof)
end
*}

end