# HG changeset patch
# User wenzelm
# Date 1003766629 -7200
# Node ID 4a8834757140084d06aa9f884805cb0799b081eb
# Parent  99569e5f0ab5bf6c1a24a67798503e795f54a043
moved prove_goalw_cterm to goals.ML;
cleaned up;

diff -r 99569e5f0ab5 -r 4a8834757140 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Mon Oct 22 18:03:21 2001 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Mon Oct 22 18:03:49 2001 +0200
@@ -9,11 +9,11 @@
 signature SKIP_PROOF =
 sig
   val quick_and_dirty: bool ref
+  val make_thm: theory -> term -> thm
+  val cheat_tac: theory -> tactic
   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;
 
@@ -27,21 +27,27 @@
 val quick_and_dirty = ref false;
 
 
-(* cheat_tac *)
+(* oracle setup *)
 
 val skip_proofN = "skip_proof";
 
-exception SkipProof;
-val any_prop = Var (("A", 0), propT);
+exception SkipProof of term;
 
-fun any_thm (_, SkipProof) =
-  if ! quick_and_dirty then any_prop
+fun skip_proof (_, SkipProof t) =
+  if ! quick_and_dirty then t
   else error "Proofs may be skipped in quick_and_dirty mode only!";
 
+val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
 
-(*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
+
+(* make_thm and cheat_tac *)
+
+fun make_thm thy t =
+  (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*)
+  Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t);
+
 fun cheat_tac thy st =
-  ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st;
+  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 
 (* "sorry" proof command *)
@@ -51,25 +57,6 @@
 val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
 val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
 
-
-(* conditional prove_goalw_cterm *)
-
-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)];
-
-
 end;