proper ML names;

--- a/src/HOL/Extraction.thy	Fri Oct 11 21:51:10 2019 +0200
+++ b/src/HOL/Extraction.thy	Fri Oct 11 22:01:45 2019 +0200
@@ -17,11 +17,11 @@
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
     Proofterm.rewrite_proof_notypes
-      ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
+      ([], Rewrite_HOL_Proof.elim_cong :: Proof_Rewrite_Rules.rprocs true) o
     Proofterm.rewrite_proof thy
-      (RewriteHOLProof.rews,
-       ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
-    ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
+      (Rewrite_HOL_Proof.rews,
+       Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]) o
+    Proof_Rewrite_Rules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
 \<close>
 
 lemmas [extraction_expand] =

--- 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;
 

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 11 21:51:10 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 11 22:01:45 2019 +0200
@@ -10,7 +10,7 @@
   val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
 end;
 
-structure RewriteHOLProof : REWRITE_HOL_PROOF =
+structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF =
 struct
 
 val rews =

--- a/src/Pure/Proof/extraction.ML	Fri Oct 11 21:51:10 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Oct 11 22:01:45 2019 +0200
@@ -505,7 +505,7 @@
     val rtypes = map fst types;
     val typroc = typeof_proc [];
     val prep = the_default (K I) prep thy' o
-      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
+      Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
       Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 
@@ -529,7 +529,7 @@
       Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
 
     fun mk_sprfs cs tye = maps (fn (_, T) =>
-      ProofRewriteRules.expand_of_sort_proof thy' (map SOME cs)
+      Proof_Rewrite_Rules.expand_of_sort_proof thy' (map SOME cs)
         (T, Sign.defaultS thy)) tye;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 21:51:10 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 22:01:45 2019 +0200
@@ -20,7 +20,7 @@
     (Proofterm.proof * Proofterm.proof) option
 end;
 
-structure ProofRewriteRules : PROOF_REWRITE_RULES =
+structure Proof_Rewrite_Rules : PROOF_REWRITE_RULES =
 struct
 
 fun rew b _ _ =