Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 37436 2d76997730a6
parent 37414 d0cea0796295
child 37479 f6b1ee5b420b 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:20:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:42:09 2010 +0200
@@ -173,7 +173,7 @@
                 (skolem_somes, @{const_name undefined})
               else case AList.find (op aconv) skolem_somes t of
                 s :: _ => (skolem_somes, s)
-              | _ =>
+              | [] =>
                 let
                   val s = skolem_theory_name ^ "." ^
                           skolem_name i (length skolem_somes)
isabelle