# HG changeset patch
# User wenzelm
# Date 1571139002 -7200
# Node ID 0b320e92485cc64a84eadebe7a10fa38342878e7
# Parent  69050518d4f33aa0feab9a7c257f55bb01433aac
tuned signature;

diff -r 69050518d4f3 -r 0b320e92485c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 15 13:11:31 2019 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 15 13:30:02 2019 +0200
@@ -70,11 +70,7 @@
 default_sort type
 setup \<open>Object_Logic.add_base_sort \<^sort>\<open>type\<close>\<close>
 
-setup \<open>
-  Proofterm.set_preproc (fn thy =>
-    Proofterm.rewrite_proof thy
-      ([], Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]))
-\<close>
+setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
 instance "fun" :: (type, type) type by (rule fun_arity)
@@ -785,12 +781,7 @@
 ML_file \<open>Tools/hologic.ML\<close>
 ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
 
-setup \<open>
-  Proofterm.set_preproc (fn thy =>
-    Proofterm.rewrite_proof thy
-      (Rewrite_HOL_Proof.rews,
-       Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]))
-\<close>
+setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc Rewrite_HOL_Proof.rews)\<close>
 
 
 subsubsection \<open>Sledgehammer setup\<close>
diff -r 69050518d4f3 -r 0b320e92485c src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Oct 15 13:11:31 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Oct 15 13:30:02 2019 +0200
@@ -18,6 +18,7 @@
   val expand_of_class_proof : theory -> term option list -> typ * class -> proof
   val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
     (Proofterm.proof * Proofterm.proof) option
+  val standard_preproc: (proof * proof) list -> theory -> proof -> proof
 end;
 
 structure Proof_Rewrite_Rules : PROOF_REWRITE_RULES =
@@ -374,4 +375,10 @@
       SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
   | expand_of_class _ _ _ _ = NONE;
 
+
+(* standard preprocessor *)
+
+fun standard_preproc rews thy =
+  Proofterm.rewrite_proof thy (rews, rprocs true @ [expand_of_class thy]);
+
 end;