# HG changeset patch
# User blanchet
# Date 1352203742 -3600
# Node ID 0ae5328ded8cea11e1e0983059afd8bdacaea8f2
# Parent  3f8ee43ac62f65d391e31323c7be68a454742753
fixed more "Trueprop" issues

diff -r 3f8ee43ac62f -r 0ae5328ded8c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 12:38:45 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 13:09:02 2012 +0100
@@ -984,23 +984,22 @@
           |> fold (fn Definition_Step _ => I (* FIXME *)
                     | Inference_Step (name as (s, ss), role, t, _, _) =>
                       Symtab.update_new (s,
-                        case resolve_conjecture ss of
-                          [j] =>
-                          if j = length hyp_ts then concl_t
-                          else nth hyp_ts j
-                        | _ =>
-                          if member (op = o apsnd fst) tainted s then
-                            t |> role <> Conjecture ? s_not
-                              |> fold exists_of (map Var (Term.add_vars t []))
-                          else
-                            t))
+                        if member (op = o apsnd fst) tainted s then
+                          t |> role <> Conjecture ? s_not
+                            |> fold exists_of (map Var (Term.add_vars t []))
+                        else
+                          t))
                   atp_proof
         (* The assumptions and conjecture are props; the rest are bools. *)
-        fun prop_of_clause c =
-          fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
-               @{term False}
-          |> (fn t => t |> fastype_of t = @{typ bool}
-                           ? (HOLogic.mk_Trueprop #> close_form))
+        fun prop_of_clause [name as (s, ss)] =
+            (case resolve_conjecture ss of
+               [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
+             | _ => the_default @{term False} (Symtab.lookup props s)
+                    |> HOLogic.mk_Trueprop |> close_form)
+          | prop_of_clause names =
+            fold (curry s_disj) (map_filter (Symtab.lookup props o fst) names)
+                 @{term False}
+            |> HOLogic.mk_Trueprop |> close_form
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
           ? cons Show