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, pos)) lthy =

  let

    val trm = ML_Context.evaluate lthy true ("r", r) txt

  in

    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy

  end

  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source

in

  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 

    OuterKeyword.thy_goal (parser >> setup_proof)

end

*}

end