# HG changeset patch
# User wenzelm
# Date 1570898472 -7200
# Node ID ef77ddd9cc6a53e50df59b20677a10c94781b0f7
# Parent  fbba2075f82313687ad08ffc0276cf652cad4426
setup preprocessing for HOL proofs;

diff -r fbba2075f823 -r ef77ddd9cc6a src/HOL/HOL.thy
--- 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>