src/HOL/Tools/inductive_realizer.ML

--- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 11 21:51:10 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 11 22:01:45 2019 +0200
@@ -269,7 +269,7 @@
   in (name, (vs,
     if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     Extraction.abs_corr_shyps thy rule vs vs2
-      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
+      (Proof_Rewrite_Rules.un_hhf_proof rlz' (attach_typeS rlz)
          (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
   end;