src/HOL/Tools/ATP/atp_problem_generate.ML

 (* not clear whether ATPs prefer to have their negative variables tagged *)
 val tag_neg_vars = false
 
 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
   | is_type_enc_higher_order _ = false
 

         | ("erased", (NONE, All_Types (* naja *))) =>
           Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
         | _ => 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
 
 fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')