src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML

       (strip_prod_type ty1 @ tys2, ty3)
     end
   | dest_fn_type ty = ([], ty)
 
 fun resolve_include_path path_prefixes path_suffix =
-  case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
+  case find_first (fn prefix => File.exists (prefix + path_suffix))
          path_prefixes of
-    SOME prefix => Path.append prefix path_suffix
+    SOME prefix => prefix + path_suffix
   | NONE => error ("Cannot find include file " ^ Path.print path_suffix)
 
 fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) =
     true
   | is_type_type (Defined_type Type_Type) = true