# 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