# HG changeset patch
# User blanchet
# Date 1386771822 -28800
# Node ID a13aa1cac0e86b1763e3e39b4911bbb338277718
# Parent  ae01c51eadffe08399c706223b2ee9bec7047889
truncate proof once False is hit to avoid confusing the rest of the code (no idea why Z3 goes on)

diff -r ae01c51eadff -r a13aa1cac0e8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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, [])