# HG changeset patch
# User wenzelm
# Date 1571139290 -7200
# Node ID de2e2382bc0d930f21368bbf84bba72278a3192c
# Parent  0b320e92485cc64a84eadebe7a10fa38342878e7
set_preproc for object-logics with type classes;

diff -r 0b320e92485c -r de2e2382bc0d src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Tue Oct 15 13:30:02 2019 +0200
+++ b/src/FOL/IFOL.thy	Tue Oct 15 13:34:50 2019 +0200
@@ -23,6 +23,7 @@
 subsection \<open>Syntax and axiomatic basis\<close>
 
 setup Pure_Thy.old_appl_syntax_setup
+setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 class "term"
 default_sort \<open>term\<close>
diff -r 0b320e92485c -r de2e2382bc0d src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Tue Oct 15 13:30:02 2019 +0200
+++ b/src/FOLP/IFOLP.thy	Tue Oct 15 13:34:50 2019 +0200
@@ -12,6 +12,7 @@
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 
 setup Pure_Thy.old_appl_syntax_setup
+setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 class "term"
 default_sort "term"
diff -r 0b320e92485c -r de2e2382bc0d src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Tue Oct 15 13:30:02 2019 +0200
+++ b/src/Sequents/LK0.thy	Tue Oct 15 13:34:50 2019 +0200
@@ -12,6 +12,8 @@
 imports Sequents
 begin
 
+setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
+
 class "term"
 default_sort "term"