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