author blanchet Wed, 11 Dec 2013 22:23:42 +0800 changeset 54715 a13aa1cac0e8 parent 54714 ae01c51eadff child 54716 55ed20a29a8c
truncate proof once False is hit to avoid confusing the rest of the code (no idea why Z3 goes on)
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 22:23:07 2013 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 22:23:42 2013 +0800
@@ -67,6 +67,12 @@
fun is_same_inference (role, t) (_, role', t', _, _) =
(t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)

+fun is_False t = t aconv @{term False} orelse t aconv @{prop False}
+
+fun truncate_at_false [] = []
+  | truncate_at_false ((line as (_, role, t, _, _)) :: lines) =
+    line :: (if role <> Conjecture andalso is_False t then [] else truncate_at_false lines)
+
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
fun add_line (name as (_, ss), role, t, rule, []) lines =
@@ -226,6 +232,7 @@
let
val atp_proof =
atp_proof
+          |> truncate_at_false
|> rpair [] |-> fold_rev add_line
|> rpair [] |-> fold_rev add_nontrivial_line
|> rpair (0, [])```