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