# HG changeset patch
# User blanchet
# Date 1351869408 -3600
# Node ID e9a9bff107da223712719cd9bed53b19f3d8d5e6
# Parent  c96e8e40d7897563107a694624ed6c9ceb2a7a70
handle non-unit clauses gracefully

diff -r c96e8e40d789 -r e9a9bff107da src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 02 16:16:48 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 02 16:16:48 2012 +0100
@@ -303,11 +303,16 @@
     [j] => (conjecture_prefix, j)
   | _ => (raw_prefix ^ ascii_of num, 0)
 
-fun add_fact_from_dependency fact_names (name as (_, ss)) =
-  if is_fact fact_names ss then
-    apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
-  else
-    apfst (insert (op =) (raw_label_for_name name))
+fun label_of_clause [name] = raw_label_for_name name
+  | label_of_clause c = (space_implode "___" (map fst c), 0)
+
+fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
+    if is_fact fact_names ss then
+      apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
+    else
+      apfst (insert (op =) (label_of_clause names))
+  | add_fact_from_dependencies fact_names names =
+    apfst (insert (op =) (label_of_clause names))
 
 fun repair_name "$true" = "c_True"
   | repair_name "$false" = "c_False"
@@ -1001,15 +1006,13 @@
                @{term False}
           |> HOLogic.mk_Trueprop
           |> close_form
-        fun label_of_clause [name] = raw_label_for_name name
-          | label_of_clause c = (space_implode "___" (map fst c), 0)
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
           ? cons Show
         fun do_have outer qs (gamma, c) =
           Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
-                 By_Metis (fold (add_fact_from_dependency fact_names
-                                 o the_single) gamma ([], [])))
+                 By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+                                ([], [])))
         fun do_inf outer (Have z) = do_have outer [] z
           | do_inf outer (Cases cases) =
             let val c = succedent_of_cases cases in