# HG changeset patch
# User berghofe
# Date 1037198075 -3600
# Node ID 82d7fc25a2250df516a040f9ca5a85cde95e7ac5
# Parent  5ace1cccb61241e406dbea1ac3efde8b98471e56
Added simple_prove_goal_cterm.

diff -r 5ace1cccb612 -r 82d7fc25a225 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Nov 13 15:34:01 2002 +0100
+++ b/src/Pure/goals.ML	Wed Nov 13 15:34:35 2002 +0100
@@ -72,6 +72,7 @@
   val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
   val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
     -> (thm list -> tactic list) -> thm
+  val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
   val push_proof	: unit -> unit
   val read		: string -> term
   val ren		: string -> int -> unit
@@ -972,6 +973,21 @@
 fun Goal s = atomic_goal (Context.the_context ()) s;
 fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s;
 
+(*simple version with minimal amount of checking and postprocessing*)
+fun simple_prove_goal_cterm G f =
+  let
+    val As = Drule.strip_imp_prems G;
+    val B = Drule.strip_imp_concl G;
+    val asms = map (norm_hhf_rule o assume) As;
+    fun check None = error "prove_goal: tactic failed"
+      | check (Some (thm, _)) = (case nprems_of thm of
+            0 => thm
+          | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
+  in
+    standard (implies_intr_list As
+      (check (Seq.pull (EVERY (f asms) (trivial B)))))
+  end;
+
 
 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
 fun by_com tac ((th,ths), pairs) : gstack =