--- a/src/HOL/HOL.thy Sat Oct 12 18:40:29 2019 +0200
+++ b/src/HOL/HOL.thy Sat Oct 12 18:41:12 2019 +0200
@@ -70,6 +70,12 @@
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>
+
axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
instance "fun" :: (type, type) type by (rule fun_arity)
@@ -779,6 +785,13 @@
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>
+
subsubsection \<open>Sledgehammer setup\<close>