# HG changeset patch
# User wenzelm
# Date 931866814 -7200
# Node ID d824a86266a90a6e397a58905275dd55adfda286
# Parent  f22a51ed9f11d673997647808b50ff38a83e1d31
added mk_cgoal, assume_goal;

diff -r f22a51ed9f11 -r d824a86266a9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 13 12:32:22 1999 +0200
+++ b/src/Pure/drule.ML	Tue Jul 13 13:53:34 1999 +0200
@@ -85,6 +85,8 @@
   val triv_goal		: thm
   val rev_triv_goal	: thm
   val mk_triv_goal      : cterm -> thm
+  val mk_cgoal		: cterm -> cterm
+  val assume_goal	: cterm -> thm
   val tvars_of_terms	: term list -> (indexname * sort) list
   val vars_of_terms	: term list -> (indexname * typ) list
   val tvars_of		: thm -> (indexname * sort) list
@@ -614,6 +616,9 @@
   val rev_triv_goal = store_thm "rev_triv_goal" (Thm.equal_elim G_def (Thm.assume G));
 end;
 
+val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign (Const ("Goal", propT --> propT)));
+fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
+
 
 
 (** variations on instantiate **)