# HG changeset patch
# User paulson
# Date 903022980 -7200
# Node ID f3f71669878e7fcb659a80e03a125364b77300eb
# Parent  3e14d6d66dab7d0e67387ffde57341385769baea
Rule mk_triv_goal for making instances of triv_goal

diff -r 3e14d6d66dab -r f3f71669878e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Aug 13 17:29:18 1998 +0200
+++ b/src/Pure/drule.ML	Thu Aug 13 17:43:00 1998 +0200
@@ -73,9 +73,10 @@
   val triv_forall_equality: thm
   val swap_prems_rl     : thm
   val equal_intr_rule   : thm
-  val triv_goal: thm
-  val rev_triv_goal: thm
-  val instantiate': ctyp option list -> cterm option list -> thm -> thm
+  val triv_goal		: thm
+  val rev_triv_goal	: thm
+  val mk_triv_goal      : cterm -> thm
+  val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
 end;
 
 structure Drule : DRULE =
@@ -630,6 +631,9 @@
     end;
 
 
+(*Make an initial proof state, "PROP A ==> (PROP A)" *)
+fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
+
 end;
 
 open Drule;
diff -r 3e14d6d66dab -r f3f71669878e src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Aug 13 17:29:18 1998 +0200
+++ b/src/Pure/goals.ML	Thu Aug 13 17:43:00 1998 +0200
@@ -61,6 +61,7 @@
   val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
   val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
   val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
+  val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
   val push_proof	: unit -> unit
   val read		: string -> term
   val ren		: string -> int -> unit
@@ -159,7 +160,7 @@
       val cAs = map (cterm_of sign) As;
       val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs;
       val cB = cterm_of sign B;
-      val st0 = let val st = Drule.instantiate' [] [Some cB] Drule.triv_goal
+      val st0 = let val st = Drule.mk_triv_goal cB
                 in  rewrite_goals_rule rths st end
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)
@@ -225,18 +226,22 @@
     Syntax is similar to "goal" command for easy keyboard use. **)
 
 (*Version taking the goal as a cterm*)
-fun prove_goalw_cterm rths chorn tacsf =
+fun prove_goalw_cterm_general check rths chorn tacsf =
   let val (prems, st0, mkresult) = prepare_proof false rths chorn
       val tac = EVERY (tacsf prems)
       fun statef() = 
 	  (case Seq.pull (tac st0) of 
 	       Some(st,_) => st
 	     | _ => error ("prove_goal: tactic failed"))
-  in  mkresult (true, cond_timeit (!proof_timing) statef)  end
+  in  mkresult (check, cond_timeit (!proof_timing) statef)  end
   handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
 	       error ("The exception above was raised for\n" ^ 
 		      string_of_cterm chorn));
 
+(*Two variants: one checking the result, one not*)
+val prove_goalw_cterm         = prove_goalw_cterm_general true
+and prove_goalw_cterm_nocheck = prove_goalw_cterm_general false;
+
 
 (*Version taking the goal as a string*)
 fun prove_goalw thy rths agoal tacsf =