theory Prove
imports Main
begin

ML {*
val r = ref (NONE:(unit -> term) option)
*}
ML {*
let
   fun setup_proof (txt, pos) lthy =
   let
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
   end;

   val setup_proof_parser = OuterParse.ML_source >> setup_proof
        
   val kind = OuterKeyword.thy_goal
in
   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
    kind setup_proof_parser
end
*}

end