src/Pure/Proof/proof_rewrite_rules.ML

       | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
 
 fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o
-      map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
+      map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
     val defnames = map Thm.derivation_name defs;
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';
         val thms = Proofterm.fold_proof_atoms true