--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Dec 14 14:33:26 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 22 17:22:09 2019 +0100
@@ -162,7 +162,7 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _)) = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Predicate_Free, _, _)) = false
| is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true
| is_type_enc_full_higher_order _ = false
fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
@@ -671,8 +671,8 @@
| _ => raise Same.SAME))
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
-fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
- | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
+fun min_hologic THF_Predicate_Free _ = THF_Predicate_Free
+ | min_hologic _ THF_Predicate_Free = THF_Predicate_Free
| min_hologic THF_Without_Choice _ = THF_Without_Choice
| min_hologic _ THF_Without_Choice = THF_Without_Choice
| min_hologic _ _ = THF_With_Choice