66 SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")" |
66 SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")" |
67 | _ => "" |
67 | _ => "" |
68 else |
68 else |
69 "") ^ "...") |
69 "") ^ "...") |
70 val {goal, ...} = Proof.goal state |
70 val {goal, ...} = Proof.goal state |
71 val facts = |
71 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) |
72 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
|
73 val params = |
72 val params = |
74 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
73 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
75 provers = provers, type_enc = type_enc, strict = strict, |
74 provers = provers, type_enc = type_enc, strict = strict, |
76 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
75 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
77 learn = false, fact_filter = NONE, max_facts = SOME (length facts), |
76 learn = false, fact_filter = NONE, max_facts = SOME (length facts), |
307 ((false, (name, params)), preplay) |
306 ((false, (name, params)), preplay) |
308 val minimize = minimize |> the_default perhaps_minimize |
307 val minimize = minimize |> the_default perhaps_minimize |
309 val (used_facts, (preplay, message, _)) = |
308 val (used_facts, (preplay, message, _)) = |
310 if minimize then |
309 if minimize then |
311 minimize_facts do_learn minimize_name params |
310 minimize_facts do_learn minimize_name params |
312 (mode <> Normal orelse not verbose) subgoal |
311 (mode <> Normal orelse not verbose) subgoal subgoal_count state |
313 subgoal_count state |
312 (filter_used_facts true used_facts (map (apsnd single) facts)) |
314 (filter_used_facts true used_facts |
|
315 (map (apsnd single o untranslated_fact) facts)) |
|
316 |>> Option.map (map fst) |
313 |>> Option.map (map fst) |
317 else |
314 else |
318 (SOME used_facts, (preplay, message, "")) |
315 (SOME used_facts, (preplay, message, "")) |
319 in |
316 in |
320 case used_facts of |
317 case used_facts of |