1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:20:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:42:09 2010 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4                  (skolem_somes, @{const_name undefined})
     1.5                else case AList.find (op aconv) skolem_somes t of
     1.6                  s :: _ => (skolem_somes, s)
     1.7 -              | _ =>
     1.8 +              | [] =>
     1.9                  let
    1.10                    val s = skolem_theory_name ^ "." ^
    1.11                            skolem_name i (length skolem_somes)