# HG changeset patch
# User desharna
# Date 1606990134 -3600
# Node ID 999b07bfd88653683f194b240d4b042bb4ba1b23
# Parent  e05b77e1ab21c302874631fb8a7d1600f23aafb6
proper renaming of THF_Lambda_Bool_Free

diff -r e05b77e1ab21 -r 999b07bfd886 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 26 18:45:19 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 03 11:08:54 2020 +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_Bool_Free, _, _, _)) = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
   | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
   | is_type_enc_full_higher_order _ = false
 fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true
@@ -695,8 +695,8 @@
   end
   handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
 
-fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free
-  | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+  | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
   | min_hologic THF_Without_Choice _ = THF_Without_Choice
   | min_hologic _ THF_Without_Choice = THF_Without_Choice
   | min_hologic _ _ = THF_With_Choice