merged

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 22 21:13:23 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 22 21:16:48 2019 +0000
@@ -32,7 +32,7 @@
      gen_simp : bool}
 
   datatype polymorphism = Monomorphic | Polymorphic
-  datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
+  datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
 
   datatype atp_format =
     CNF |
@@ -188,7 +188,7 @@
    gen_simp : bool}
 
 datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
 
 datatype atp_format =
   CNF |

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 21:13:23 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 21:16:48 2019 +0000
@@ -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
@@ -2614,7 +2614,7 @@
       else
         Sufficient_App_Op_And_Predicator
     val lam_trans =
-      if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
+      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
       else lam_trans
     val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
       translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 22 21:13:23 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 22 21:16:48 2019 +0000
@@ -354,7 +354,7 @@
 
 (* Ehoh *)
 
-val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free)
+val ehoh_thf0 = THF (Monomorphic, THF_Predicate_Free)
 
 val ehoh_config : atp_config =
   {exec = fn _ => (["E_HOME"], ["eprover"]),
@@ -443,7 +443,7 @@
 
 (* Leo-III *)
 
-(* include choice? Disabled now since its disabled for satallax as well. *)
+(* Include choice? Disabled now since it's disabled for Satallax as well. *)
 val leo3_thf1 = THF (Polymorphic, THF_Without_Choice)
 
 val leo3_config : atp_config =
@@ -627,7 +627,9 @@
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
 
 
-(* Zipperposition*)
+(* Zipperposition *)
+
+val zipperposition_thf1 = THF (Polymorphic, THF_Predicate_Free)
 
 val zipperposition_config : atp_config =
   {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
@@ -639,7 +641,7 @@
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
+     [(1.0, (((100, ""), zipperposition_thf1, "poly_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 

--- a/src/Pure/Isar/toplevel.ML	Tue Jan 22 21:13:23 2019 +0000
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 22 21:16:48 2019 +0000
@@ -749,6 +749,5 @@
 end;
 
 end;
-(* FIXME
+
 structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;
-*)