# HG changeset patch
# User wenzelm
# Date 1303243722 -7200
# Node ID 3e1e80df6a4259f302f18bc47e5d166116923b52
# Parent  282b7a3065d3c9055ddb407430ad93d183f4af89
added more elementary Skip_Proof.make_thm_cterm;

diff -r 282b7a3065d3 -r 3e1e80df6a42 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Tue Apr 19 21:55:42 2011 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Tue Apr 19 22:08:42 2011 +0200
@@ -7,6 +7,7 @@
 
 signature SKIP_PROOF =
 sig
+  val make_thm_cterm: cterm -> thm
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
   val prove: Proof.context -> string list -> term list -> term ->
@@ -20,14 +21,14 @@
 
 (* oracle setup *)
 
-val (_, skip_proof) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
+val (_, make_thm_cterm) =
+  Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
+
+fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
 
 
 (* basic cheating *)
 
-fun make_thm thy prop = skip_proof (thy, prop);
-
 fun cheat_tac thy st =
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;