src/Pure/Isar/element.ML

     Drule.forall_elim_list (map (cert o snd) subst)
   end;
 
 fun hyps_rule rule th =
   let
-    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
+    val cterm_rule = Drule.mk_term #> rule #> Drule.dest_term;
     val {hyps, ...} = Thm.crep_thm th;
   in
     Drule.implies_elim_list
       (rule (Drule.implies_intr_list hyps th))
       (map (Thm.assume o cterm_rule) hyps)