src/Pure/drule.ML
changeset 12092 d1896409ff13
parent 12054 a96c9563d568
child 12126 34f72eb7d2db
     1.1 --- a/src/Pure/drule.ML	Wed Nov 07 18:17:16 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Nov 07 18:17:45 2001 +0100
     1.3 @@ -330,7 +330,8 @@
     1.4  
     1.5  (* maps |- B to A1,...,An |- B *)
     1.6  fun impose_hyps chyps th =
     1.7 -  implies_elim_list (implies_intr_list chyps th) (map Thm.assume chyps);
     1.8 +  let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th))
     1.9 +  in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end;
    1.10  
    1.11  (*Reset Var indexes to zero, renaming to preserve distinctness*)
    1.12  fun zero_var_indexes th =