author | blanchet |
Fri, 09 Sep 2011 14:30:57 +0200 | |
changeset 44853 | e3310cdb4e48 |
parent 44852 | 8ac91e7b6024 |
child 44856 | 3d44712a5f66 |
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Sep 08 12:23:11 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Sep 09 14:30:57 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