Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorbulwahn
Fri, 09 Sep 2011 15:14:59 +0200
changeset 44856 3d44712a5f66
parent 44855 f4a6786057d9 (current diff)
parent 44853 e3310cdb4e48 (diff)
child 44857 73d5b722c4b4
merged
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Sep 09 14:43:50 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Sep 09 15:14:59 2011 +0200
@@ -1899,7 +1899,8 @@
            let
              val (pred_sym, in_conj) =
                case Symtab.lookup sym_tab s of
-                 SOME {pred_sym, in_conj, ...} => (pred_sym, in_conj)
+                 SOME ({pred_sym, in_conj, ...} : sym_info) =>
+                 (pred_sym, in_conj)
                | NONE => (false, false)
              val decl_sym =
                (case type_enc of
isabelle