--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Aug 02 17:20:16 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 03 09:22:38 2021 +0200
@@ -55,6 +55,7 @@
val zipperpositionN : string
val remote_prefix : string
val dummy_tfxN : string
+ val dummy_thfN : string
val agsyhol_core_rule : string
val spass_input_rule : string
@@ -117,6 +118,7 @@
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
val dummy_tfxN = "dummy_tfx"
+val dummy_thfN = "dummy_thf"
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val spass_input_rule = "Inp"