exception SkipProof of term;

 val (_, skip_proof) = Context.>>> (Context.map_theory_result

   (Thm.add_oracle ("skip_proof", fn (thy, prop) =>

 fun skip_proof (_, SkipProof prop) =

     if ! quick_and_dirty then Thm.cterm_of thy prop

   if ! quick_and_dirty then prop

     else error "Proof may be skipped in quick_and_dirty mode only!")));

   else error "Proof may be skipped in quick_and_dirty mode only!";

 val _ = Context.>> (Context.map_theory

   (Theory.add_oracle ("skip_proof", skip_proof)));

 fun make_thm thy prop =

 fun make_thm thy prop = skip_proof (thy, prop);

   Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);