Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 80910 406a85a25189
parent 69593 3dda49e08b9d 
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -411,7 +411,7 @@
   case x of
       Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
         "(" ^ string_of_symbol symbol ^ " " ^
-        space_implode " " (map string_of_tptp_type tptp_type_list
+        implode_space (map string_of_tptp_type tptp_type_list
           @ map string_of_tptp_term tptp_term_list) ^ ")"
     | Term_Var str => str
     | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
@@ -496,11 +496,11 @@
 
 and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
       "(" ^ string_of_symbol symbol ^
-      space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
+      implode_space (map string_of_tptp_term tptp_term_list) ^ ")"
   | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
       "(" ^
       string_of_symbol symbol ^
-      space_implode " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
+      implode_space (map string_of_tptp_formula tptp_formula_list) ^ ")"
   | string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
   | string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
       string_of_quantifier quantifier ^ "[" ^
isabelle