src/HOL/Tools/res_atp.ML

--- 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 =