# HG changeset patch
# User bulwahn
# Date 1315574099 -7200
# Node ID 3d44712a5f66375075ffbb3de26bc488f015d14b
# Parent  f4a6786057d9cd39aedbbae361ff4a4adc4809c2# Parent  e3310cdb4e48f87cc789d368b8a49c421865ed24
merged

diff -r f4a6786057d9 -r 3d44712a5f66 src/HOL/Tools/ATP/atp_translate.ML
--- 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