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