src/Pure/Isar/skip_proof.ML

   val quick_and_dirty: bool ref
   val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     -> Proof.state -> Proof.state Seq.seq
   val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm
+  val make_thm: theory -> term -> thm
   val setup: (theory -> theory) list
 end;
 
 structure SkipProof: SKIP_PROOF =
 struct

 fun prove_goalw_cterm thy rews ct tacs =
   Goals.prove_goalw_cterm rews ct
     (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs);
 
 
+(* make_thm *)
+
+fun make_thm thy t =
+  prove_goalw_cterm thy [] (Thm.cterm_of (Theory.sign_of thy) t) (K []);
+
+
 (* theory setup *)
 
 val setup = [Theory.add_oracle (skip_proofN, any_thm)];