src/HOL/TPTP/atp_problem_import.ML

--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -39,12 +39,6 @@
 
 (** TPTP parsing **)
 
-(* cf. "close_form" in "refute.ML" *)
-fun close_form t =
-  fold (fn ((s, i), T) => fn t' =>
-           Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
-       (Term.add_vars t []) t
-
 fun read_tptp_file thy postproc file_name =
   let
     fun has_role role (_, role', _, _) = (role' = role)