--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
@@ -41,18 +41,18 @@
val no_type_enc : string
val full_type_encs : string list
val partial_type_encs : string list
+ val metis_default_lam_trans : string
+ val metis_call : string -> string -> string
+ val string_for_reconstructor : reconstructor -> string
val used_facts_in_atp_proof :
Proof.context -> (string * locality) list vector -> string proof
-> (string * locality) list
- val is_axiom_used_in_proof : (string list -> bool) -> 'a proof -> bool
- val is_typed_helper : string list -> bool
+ val lam_trans_from_atp_proof : string proof -> string -> string
+ val is_typed_helper_used_in_proof : string proof -> bool
val used_facts_in_unsound_atp_proof :
Proof.context -> (string * locality) list vector -> 'a proof
-> string list option
val unalias_type_enc : string -> string list
- val metis_default_lam_trans : string
- val metis_call : string -> string -> string
- val name_of_reconstructor : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
@@ -92,79 +92,6 @@
bool * int * string Symtab.table * (string * locality) list vector
* int Symtab.table * string proof * thm
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
-val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
-
-fun resolve_one_named_fact fact_names s =
- case try (unprefix fact_prefix) s of
- SOME s' =>
- let val s' = s' |> unprefix_fact_number |> unascii_of in
- s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
- end
- | NONE => NONE
-fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
-val is_fact = not o null oo resolve_fact
-
-fun resolve_one_named_conjecture s =
- case try (unprefix conjecture_prefix) s of
- SOME s' => Int.fromString s'
- | NONE => NONE
-
-val resolve_conjecture = map_filter resolve_one_named_conjecture
-val is_conjecture = not o null o resolve_conjecture
-
-val is_typed_helper_name =
- String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
-val is_typed_helper = exists is_typed_helper_name
-
-val leo2_ext = "extcnf_equal_neg"
-val isa_ext = Thm.get_name_hint @{thm ext}
-val isa_short_ext = Long_Name.base_name isa_ext
-
-fun ext_name ctxt =
- if Thm.eq_thm_prop (@{thm ext},
- singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
- isa_short_ext
- else
- isa_ext
-
-fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) =
- union (op =) (resolve_fact fact_names ss)
- | add_fact ctxt _ (Inference (_, _, rule, _)) =
- if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
- | add_fact _ _ _ = I
-
-fun used_facts_in_atp_proof ctxt fact_names atp_proof =
- if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
- else fold (add_fact ctxt fact_names) atp_proof []
-
-fun is_axiom_used_in_proof pred =
- exists (fn Inference ((_, ss), _, _, []) => pred ss | _ => false)
-
-(* (quasi-)underapproximation of the truth *)
-fun is_locality_global Local = false
- | is_locality_global Assum = false
- | is_locality_global Chained = false
- | is_locality_global _ = true
-
-fun used_facts_in_unsound_atp_proof _ _ [] = NONE
- | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
- let
- val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
- in
- if forall (is_locality_global o snd) used_facts andalso
- not (is_axiom_used_in_proof is_conjecture atp_proof) then
- SOME (map fst used_facts)
- else
- NONE
- end
-
-
-(** Soft-core proof reconstruction: one-liners **)
-
val metisN = "metis"
val smtN = "smt"
@@ -201,10 +128,96 @@
|> lam_trans <> metis_default_lam_trans ? cons lam_trans
in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-(* unfortunate leaking abstraction *)
-fun name_of_reconstructor (Metis (type_enc, lam_trans)) =
+fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
metis_call type_enc lam_trans
- | name_of_reconstructor SMT = smtN
+ | string_for_reconstructor SMT = smtN
+
+fun find_first_in_list_vector vec key =
+ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+ | (_, value) => value) NONE vec
+
+val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+
+fun resolve_one_named_fact fact_names s =
+ case try (unprefix fact_prefix) s of
+ SOME s' =>
+ let val s' = s' |> unprefix_fact_number |> unascii_of in
+ s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
+ end
+ | NONE => NONE
+fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
+val is_fact = not o null oo resolve_fact
+
+fun resolve_one_named_conjecture s =
+ case try (unprefix conjecture_prefix) s of
+ SOME s' => Int.fromString s'
+ | NONE => NONE
+
+val resolve_conjecture = map_filter resolve_one_named_conjecture
+val is_conjecture = not o null o resolve_conjecture
+
+fun is_axiom_used_in_proof pred =
+ exists (fn Inference ((_, ss), _, _, []) => exists pred ss | _ => false)
+
+val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
+
+val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
+
+(* overapproximation (good enough) *)
+fun is_lam_lifted s =
+ String.isPrefix fact_prefix s andalso
+ String.isSubstring ascii_of_lam_fact_prefix s
+
+fun lam_trans_from_atp_proof atp_proof default =
+ if is_axiom_used_in_proof is_combinator_def atp_proof then combinatorsN
+ else if is_axiom_used_in_proof is_lam_lifted atp_proof then lam_liftingN
+ else default
+
+val is_typed_helper_name =
+ String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+val is_typed_helper_used_in_proof = is_axiom_used_in_proof is_typed_helper_name
+
+val leo2_ext = "extcnf_equal_neg"
+val isa_ext = Thm.get_name_hint @{thm ext}
+val isa_short_ext = Long_Name.base_name isa_ext
+
+fun ext_name ctxt =
+ if Thm.eq_thm_prop (@{thm ext},
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ isa_short_ext
+ else
+ isa_ext
+
+fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) =
+ union (op =) (resolve_fact fact_names ss)
+ | add_fact ctxt _ (Inference (_, _, rule, _)) =
+ if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
+ | add_fact _ _ _ = I
+
+fun used_facts_in_atp_proof ctxt fact_names atp_proof =
+ if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
+ else fold (add_fact ctxt fact_names) atp_proof []
+
+(* (quasi-)underapproximation of the truth *)
+fun is_locality_global Local = false
+ | is_locality_global Assum = false
+ | is_locality_global Chained = false
+ | is_locality_global _ = true
+
+fun used_facts_in_unsound_atp_proof _ _ [] = NONE
+ | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
+ let
+ val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
+ in
+ if forall (is_locality_global o snd) used_facts andalso
+ not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
+ SOME (map fst used_facts)
+ else
+ NONE
+ end
+
+
+(** Soft-core proof reconstruction: one-liners **)
fun string_for_label (s, num) = s ^ string_of_int num
@@ -225,7 +238,7 @@
"using " ^ space_implode " " (map string_for_label ls) ^ " "
fun reconstructor_command reconstr i n (ls, ss) =
using_labels ls ^ apply_on_subgoal i n ^
- command_call (name_of_reconstructor reconstr) ss
+ command_call (string_for_reconstructor reconstr) ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -344,8 +357,8 @@
fun num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
- else if String.isPrefix lambda_lifted_prefix s then
- if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
+ else if String.isPrefix lam_lifted_prefix s then
+ if String.isPrefix lam_lifted_poly_prefix s then 2 else 0
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
@@ -945,7 +958,7 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt0 full_types i n =
+fun string_for_proof ctxt0 type_enc lam_trans i n =
let
val ctxt =
ctxt0 |> Config.put show_free_types false
@@ -967,8 +980,7 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstr =
- Metis (if full_types then full_typesN else partial_typesN, combinatorsN)
+ val reconstr = Metis (type_enc, lam_trans)
fun do_facts (ls, ss) =
reconstructor_command reconstr 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
@@ -1013,7 +1025,10 @@
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val one_line_proof = one_line_proof_text one_line_params
- val full_types = is_axiom_used_in_proof is_typed_helper atp_proof
+ val type_enc =
+ if is_typed_helper_used_in_proof atp_proof then full_typesN
+ else partial_typesN
+ val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
fun isar_proof_for () =
case atp_proof
|> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names
@@ -1023,7 +1038,7 @@
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt full_types subgoal subgoal_count of
+ |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count of
"" =>
if isar_proof_requested then
"\nNo structured proof available (proof too short)."
--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 11:47:12 2011 +0100
@@ -44,12 +44,13 @@
val const_prefix : string
val type_const_prefix : string
val class_prefix : string
- val lambda_lifted_prefix : string
- val lambda_lifted_mono_prefix : string
- val lambda_lifted_poly_prefix : string
+ val lam_lifted_prefix : string
+ val lam_lifted_mono_prefix : string
+ val lam_lifted_poly_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
+ val combinator_prefix : string
val type_decl_prefix : string
val sym_decl_prefix : string
val guards_sym_formula_prefix : string
@@ -60,7 +61,7 @@
val class_rel_clause_prefix : string
val arity_clause_prefix : string
val tfree_clause_prefix : string
- val lambda_fact_prefix : string
+ val lam_fact_prefix : string
val typed_helper_suffix : string
val untyped_helper_suffix : string
val type_tag_idempotence_helper_name : string
@@ -146,14 +147,16 @@
(* Freshness almost guaranteed! *)
val atp_weak_prefix = "ATP:"
-val lambda_lifted_prefix = atp_weak_prefix ^ "Lam"
-val lambda_lifted_mono_prefix = lambda_lifted_prefix ^ "m"
-val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "p"
+val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
+val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
+val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
+val combinator_prefix = "COMB"
+
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val guards_sym_formula_prefix = "gsy_"
@@ -165,7 +168,7 @@
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"
-val lambda_fact_prefix = "ATP.lambda_"
+val lam_fact_prefix = "ATP.lambda_"
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
@@ -272,11 +275,11 @@
(@{const_name Ex}, "Ex"),
(@{const_name If}, "If"),
(@{const_name Set.member}, "member"),
- (@{const_name Meson.COMBI}, "COMBI"),
- (@{const_name Meson.COMBK}, "COMBK"),
- (@{const_name Meson.COMBB}, "COMBB"),
- (@{const_name Meson.COMBC}, "COMBC"),
- (@{const_name Meson.COMBS}, "COMBS")]
+ (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
+ (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
+ (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
+ (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
+ (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
|> Symtab.make
|> fold (Symtab.update o swap o snd o snd o snd) proxy_table
@@ -488,7 +491,7 @@
fun robust_const_type thy s =
if s = app_op_name then
Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
- else if String.isPrefix lambda_lifted_prefix s then
+ else if String.isPrefix lam_lifted_prefix s then
Logic.varifyT_global @{typ "'a => 'b"}
else
(* Old Skolems throw a "TYPE" exception here, which will be caught. *)
@@ -500,8 +503,8 @@
let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
else if String.isPrefix old_skolem_const_prefix s then
[] |> Term.add_tvarsT T |> rev |> map TVar
- else if String.isPrefix lambda_lifted_prefix s then
- if String.isPrefix lambda_lifted_poly_prefix s then
+ else if String.isPrefix lam_lifted_prefix s then
+ if String.isPrefix lam_lifted_poly_prefix s then
let val (T1, T2) = T |> dest_funT in [T1, T2] end
else
[]
@@ -678,7 +681,7 @@
fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
| constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
| constify_lifted (Free (x as (s, _))) =
- (if String.isPrefix lambda_lifted_prefix s then Const else Free) x
+ (if String.isPrefix lam_lifted_prefix s then Const else Free) x
| constify_lifted t = t
(* Requires bound variables to have distinct names and not to clash with any
@@ -687,15 +690,17 @@
open_form (subst_bound (Var ((s, 0), T), t))
| open_form t = t
-fun lift_lams ctxt type_enc =
+fun lift_lams_part_1 ctxt type_enc =
map (Envir.eta_contract #> close_form) #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
(SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
- lambda_lifted_poly_prefix
+ lam_lifted_poly_prefix
else
- lambda_lifted_mono_prefix))
+ lam_lifted_mono_prefix))
Lambda_Lifting.is_quantifier
- #> fst #> pairself (map (open_form o constify_lifted))
+ #> fst
+val lift_lams_part_2 = pairself (map (open_form o constify_lifted))
+val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
intentionalize_def t
@@ -1146,7 +1151,7 @@
do_cheaply_conceal_lambdas Ts t1
$ do_cheaply_conceal_lambdas Ts t2
| do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
- Const (lambda_lifted_poly_prefix ^ serial_string (),
+ Const (lam_lifted_poly_prefix ^ serial_string (),
T --> fastype_of1 (T :: Ts, t))
| do_cheaply_conceal_lambdas _ t = t
@@ -1167,11 +1172,11 @@
val (facts, lambda_ts) =
facts |> map (snd o snd) |> trans_lams
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
- val lambda_facts =
+ val lam_facts =
map2 (fn t => fn j =>
- ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
+ ((lam_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
lambda_ts (1 upto length lambda_ts)
- in (facts, lambda_facts) end
+ in (facts, lam_facts) end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
@@ -1684,8 +1689,9 @@
else if lam_trans = combinatorsN then
map (introduce_combinators ctxt) #> rpair []
else if lam_trans = hybrid_lamsN then
- lift_lams ctxt type_enc
+ lift_lams_part_1 ctxt type_enc
##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
+ #> lift_lams_part_2
else if lam_trans = keep_lamsN then
map (Envir.eta_contract) #> rpair []
else
@@ -1708,7 +1714,7 @@
map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
|> map (apsnd freeze_term)
|> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
- val ((conjs, facts), lambda_facts) =
+ val ((conjs, facts), lam_facts) =
(conjs, facts)
|> presimp
? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
@@ -1725,10 +1731,9 @@
make_fact ctxt format type_enc true (name, t)
|> Option.map (pair name))
|> ListPair.unzip
- val lifted = lambda_facts |> map (extract_lambda_def o snd o snd)
- val lambda_facts =
- lambda_facts
- |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
+ val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
+ val lam_facts =
+ lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
val all_ts = concl_t :: hyp_ts @ fact_ts
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
@@ -1739,7 +1744,7 @@
val class_rel_clauses = make_class_rel_clauses thy subs supers
in
(fact_names |> map single, union (op =) subs supers, conjs,
- facts @ lambda_facts, class_rel_clauses, arity_clauses, lifted)
+ facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
end
val type_guard = `(make_fixed_const NONE) type_guard_name
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100
@@ -112,7 +112,7 @@
fun reveal_lambda_lifted lambdas =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix lam_lifted_prefix s then
case AList.lookup (op =) lambdas s of
SOME t =>
Const (@{const_name Metis.lambda}, dummyT)
@@ -189,7 +189,7 @@
SOME j =>
Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
| NONE =>
- if String.isPrefix lambda_fact_prefix (unascii_of s) then
+ if String.isPrefix lam_fact_prefix (unascii_of s) then
Isa_Lambda_Lifted |> some
else
raise Fail ("malformed fact identifier " ^ quote ident)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
@@ -145,14 +145,14 @@
val reconstructor_names = [metisN, smtN]
val plain_metis = Metis (hd partial_type_encs, combinatorsN)
-fun bunch_of_reconstructors full_types lam_trans =
- if full_types then
- [Metis (hd full_type_encs, lam_trans)]
- else
- [Metis (hd partial_type_encs, lam_trans),
- Metis (hd full_type_encs, lam_trans),
- Metis (no_type_enc, lam_trans),
- SMT]
+fun bunch_of_reconstructors needs_full_types lam_trans =
+ [(false, Metis (hd partial_type_encs, lam_trans metis_default_lam_trans)),
+ (true, Metis (hd full_type_encs, lam_trans metis_default_lam_trans)),
+ (false, Metis (no_type_enc, lam_trans hide_lamsN)),
+ (true, SMT)]
+ |> map_filter (fn (full_types, reconstr) =>
+ if needs_full_types andalso not full_types then NONE
+ else SOME reconstr)
val is_reconstructor = member (op =) reconstructor_names
val is_atp = member (op =) o supported_atps
@@ -451,7 +451,7 @@
let
val _ =
if verbose then
- "Trying \"" ^ name_of_reconstructor reconstr ^ "\" for " ^
+ "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
string_from_time timeout ^ "..."
|> Output.urgent_message
else
@@ -734,7 +734,7 @@
| NONE => NONE)
| _ => outcome
in
- ((pool, fact_names, sym_tab, lam_trans),
+ ((pool, fact_names, sym_tab),
(output, run_time, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
@@ -753,7 +753,7 @@
end
| maybe_run_slice _ result = result
in
- ((Symtab.empty, Vector.fromList [], Symtab.empty, no_lamsN),
+ ((Symtab.empty, Vector.fromList [], Symtab.empty),
("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
@@ -769,8 +769,7 @@
()
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
- val ((pool, fact_names, sym_tab, lam_trans),
- (output, run_time, atp_proof, outcome)) =
+ val ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
if mode = Normal andalso
@@ -783,11 +782,10 @@
NONE =>
let
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
- val full_types = is_axiom_used_in_proof is_typed_helper atp_proof
+ val needs_full_types = is_typed_helper_used_in_proof atp_proof
val reconstrs =
- bunch_of_reconstructors full_types
- (if member (op =) metis_lam_transs lam_trans then lam_trans
- else combinatorsN)
+ bunch_of_reconstructors needs_full_types
+ (lam_trans_from_atp_proof atp_proof)
in
(used_facts,
fn () =>
@@ -976,8 +974,8 @@
NONE =>
(fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal SMT
- (bunch_of_reconstructors false lam_liftingN),
+ state subgoal SMT
+ (bunch_of_reconstructors false (K lam_liftingN)),
fn preplay =>
let
val one_line_params =