# HG changeset patch
# User wenzelm
# Date 1002881378 -7200
# Node ID 139aaced13f4522d33826330e45976bc0e14088e
# Parent  1a0c1ef8651896f52d6c18cbee342b9229feca97
added make_thm (sort-of);

diff -r 1a0c1ef86518 -r 139aaced13f4 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Fri Oct 12 12:09:21 2001 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 12 12:09:38 2001 +0200
@@ -13,6 +13,7 @@
     -> 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;
 
@@ -58,6 +59,12 @@
     (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)];