author | wenzelm |
Thu, 14 Sep 2006 00:23:02 +0200 | |
changeset 20532 | 64181717e37c |
parent 20531 | 7de9caf4fd78 |
child 20533 | 49442b3024bb |
--- a/src/HOL/Tools/res_atp.ML Wed Sep 13 21:41:31 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Sep 14 00:23:02 2006 +0200 @@ -619,7 +619,7 @@ (*Ensures that no higher-order theorems "leak out"*) fun restrict_to_logic logic cls = - if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls + if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls else cls; fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =