src/HOL/Tools/res_atp.ML
changeset 20532 64181717e37c
parent 20526 756c4f1fd04c
child 20643 267f30cbe2cb
equal deleted inserted replaced
20531:7de9caf4fd78 20532:64181717e37c
   617 
   617 
   618 val linkup_logic_mode = ref Auto;
   618 val linkup_logic_mode = ref Auto;
   619 
   619 
   620 (*Ensures that no higher-order theorems "leak out"*)
   620 (*Ensures that no higher-order theorems "leak out"*)
   621 fun restrict_to_logic logic cls =
   621 fun restrict_to_logic logic cls =
   622   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls 
   622   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   623 	                else cls;
   623 	                else cls;
   624 
   624 
   625 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   625 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   626     if is_fol_logic logic 
   626     if is_fol_logic logic 
   627     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   627     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)