60 let val (_, hyp_ts, concl_t) = strip_subgoal goal i in |
60 let val (_, hyp_ts, concl_t) = strip_subgoal goal i in |
61 not (forall (Meson.is_fol_term thy) |
61 not (forall (Meson.is_fol_term thy) |
62 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
62 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
63 end |
63 end |
64 val params = |
64 val params = |
65 {debug = debug, verbose = false, overlord = overlord, blocking = true, |
65 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
66 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
66 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
67 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
67 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
68 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
68 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
69 timeout = timeout, expect = ""} |
69 timeout = timeout, expect = ""} |
70 val facts = |
70 val facts = |