diff -r eff0ede61da1 -r 0cbda884a7e5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 18 12:05:29 2002 +0200
+++ b/src/Pure/drule.ML	Thu Jul 18 12:05:51 2002 +0200
@@ -101,6 +101,7 @@
   val kind_internal: 'a attribute
   val has_internal: tag list -> bool
   val impose_hyps: cterm list -> thm -> thm
+  val satisfy_hyps: thm list -> thm -> thm
   val close_derivation: thm -> thm
   val local_standard: thm -> thm
   val compose_single: thm * int * thm -> thm
@@ -350,6 +351,10 @@
   let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th))
   in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end;
 
+(* maps A1,...,An and A1,...,An |- B to |- B *)
+fun satisfy_hyps ths th =
+  implies_elim_list (implies_intr_list (map (#prop o Thm.crep_thm) ths) th) ths;
+
 (*Reset Var indexes to zero, renaming to preserve distinctness*)
 fun zero_var_indexes th =
     let val {prop,sign,...} = rep_thm th;