src/HOL/Tools/res_atp.ML
changeset 20532 64181717e37c
parent 20526 756c4f1fd04c
child 20643 267f30cbe2cb
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 13 21:41:31 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 14 00:23:02 2006 +0200
     1.3 @@ -619,7 +619,7 @@
     1.4  
     1.5  (*Ensures that no higher-order theorems "leak out"*)
     1.6  fun restrict_to_logic logic cls =
     1.7 -  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls 
     1.8 +  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
     1.9  	                else cls;
    1.10  
    1.11  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =