# HG changeset patch
# User wenzelm
# Date 1131442989 -3600
# Node ID 38316c575328283e6071102eff848ee0877c8fc9
# Parent  61a430a67d7c0e3cc5203247e688f6b3fc1ea31b
removed impose_hyps, satisfy_hyps;
tuned;

diff -r 61a430a67d7c -r 38316c575328 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Nov 08 10:43:08 2005 +0100
+++ b/src/Pure/drule.ML	Tue Nov 08 10:43:09 2005 +0100
@@ -108,8 +108,6 @@
   val internalK: string
   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 flexflex_unique: thm -> thm
   val close_derivation: thm -> thm
   val local_standard: thm -> thm
@@ -410,7 +408,7 @@
   in fold elim (outer_params prop) th end;
 
 (*lift vars wrt. outermost goal parameters
-  -- reverses the effect of gen_all modulo HO unification*)
+  -- reverses the effect of gen_all modulo higher-order unification*)
 fun lift_all goal th =
   let
     val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
@@ -436,13 +434,6 @@
 (*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
 fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
 
-(*maps |- B to A1,...,An |- B*)
-val impose_hyps = fold Thm.weaken;
-
-(* 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
@@ -969,9 +960,12 @@
 end;
 
 fun implies_intr_protected asms th =
-  implies_elim_list (implies_intr_list asms th)
-    (map (fn ct => Thm.assume (protect ct) RS protectD) asms)
-  |> implies_intr_list (map protect asms);
+  let val asms' = map protect asms in
+    implies_elim_list
+      (implies_intr_list asms th)
+      (map (fn asm' => Thm.assume asm' RS protectD) asms')
+    |> implies_intr_list asms'
+  end;
 
 
 (** variations on instantiate **)