src/HOL/Tools/SMT2/smtlib2_isar.ML

   val simplify_bool: term -> term
   val unlift_term: term list -> term -> term
   val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term
   val normalizing_prems : Proof.context -> term -> (string * string list) list
   val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
-    (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c
+    (''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
   val unskolemize_names: term -> term
 end;
 
 structure SMTLIB2_Isar: SMTLIB2_ISAR =
 struct

       NONE)
 
 fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t
     t =
   (case ss of
-    [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
+    [s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s))
   | _ =>
     if id = conjecture_id then
-      (Conjecture, concl_t)
+      SOME (Conjecture, concl_t)
     else
-      (Hypothesis,
-       (case find_index (curry (op =) id) prem_ids of
-         ~1 => t
-       | i => nth hyp_ts i)))
+     (case find_index (curry (op =) id) prem_ids of
+       ~1 => NONE (* lambda-lifting definition *)
+     | i => SOME (Hypothesis, nth hyp_ts i)))
 
 end;