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;