1structure holmakebuild =
2struct
3
4local
5   open Feedback
6
7   val holmake_tag = "tactic_failed"
8
9   fun basic_prover (t, tac: Abbrev.tactic) =
10     Tactical.default_prover (t, tac)
11     handle (e as HOL_ERR _) =>
12        (HOL_MESG
13           ("*** Proof of \n  " ^ Parse.term_to_string t ^ "\n*** failed (used CHEAT).\n")
14         ; HOL_MESG (exn_to_string e)
15         ; Thm.mk_oracle_thm holmake_tag ([], t))
16in
17   val () = Tactical.set_prover basic_prover
18end
19
20end
21