# HG changeset patch
# User wenzelm
# Date 1004134006 -7200
# Node ID 58ffa8bec4da1718f187843a02d3532d97a47420
# Parent  ed914e8a0fd11301710662d12499fbf3a2b7e374
added impose_hyps;

diff -r ed914e8a0fd1 -r 58ffa8bec4da src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Oct 27 00:06:22 2001 +0200
+++ b/src/Pure/drule.ML	Sat Oct 27 00:06:46 2001 +0200
@@ -97,6 +97,7 @@
   val internalK         : string
   val kind_internal     : 'a attribute
   val has_internal      : tag list -> bool
+  val impose_hyps       : cterm list -> thm -> thm
   val close_derivation  : thm -> thm
   val compose_single    : thm * int * thm -> thm
   val add_rules         : thm list -> thm list -> thm list
@@ -318,6 +319,10 @@
 (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
 fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
 
+(* maps |- B to A1,...,An |- B *)
+fun impose_hyps chyps th =
+  implies_elim_list (implies_intr_list chyps th) (map Thm.assume chyps);
+
 (*Reset Var indexes to zero, renaming to preserve distinctness*)
 fun zero_var_indexes th =
     let val {prop,sign,...} = rep_thm th;