1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 02 16:16:48 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Nov 02 16:16:48 2012 +0100
     1.3 @@ -303,11 +303,16 @@
     1.4      [j] => (conjecture_prefix, j)
     1.5    | _ => (raw_prefix ^ ascii_of num, 0)
     1.6  
     1.7 -fun add_fact_from_dependency fact_names (name as (_, ss)) =
     1.8 -  if is_fact fact_names ss then
     1.9 -    apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
    1.10 -  else
    1.11 -    apfst (insert (op =) (raw_label_for_name name))
    1.12 +fun label_of_clause [name] = raw_label_for_name name
    1.13 +  | label_of_clause c = (space_implode "___" (map fst c), 0)
    1.14 +
    1.15 +fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
    1.16 +    if is_fact fact_names ss then
    1.17 +      apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
    1.18 +    else
    1.19 +      apfst (insert (op =) (label_of_clause names))
    1.20 +  | add_fact_from_dependencies fact_names names =
    1.21 +    apfst (insert (op =) (label_of_clause names))
    1.22  
    1.23  fun repair_name "$true" = "c_True"
    1.24    | repair_name "$false" = "c_False"
    1.25 @@ -1001,15 +1006,13 @@
    1.26                 @{term False}
    1.27            |> HOLogic.mk_Trueprop
    1.28            |> close_form
    1.29 -        fun label_of_clause [name] = raw_label_for_name name
    1.30 -          | label_of_clause c = (space_implode "___" (map fst c), 0)
    1.31          fun maybe_show outer c =
    1.32            (outer andalso length c = 1 andalso subset (op =) (c, conjs))
    1.33            ? cons Show
    1.34          fun do_have outer qs (gamma, c) =
    1.35            Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
    1.36 -                 By_Metis (fold (add_fact_from_dependency fact_names
    1.37 -                                 o the_single) gamma ([], [])))
    1.38 +                 By_Metis (fold (add_fact_from_dependencies fact_names) gamma
    1.39 +                                ([], [])))
    1.40          fun do_inf outer (Have z) = do_have outer [] z
    1.41            | do_inf outer (Cases cases) =
    1.42              let val c = succedent_of_cases cases in