Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper ml_source: avoid duplicate Bash.string;
authorwenzelm
Sun, 20 Sep 2020 20:00:14 +0200
changeset 72277 48254fa33d88
parent 72276 dfe150a246e6
child 72278 199dc903131b
proper ml_source: avoid duplicate Bash.string;
src/HOL/Library/code_test.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/code_test.ML	Sun Sep 20 19:36:45 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Sun Sep 20 20:00:14 2020 +0200
@@ -395,8 +395,8 @@
       "end;"
     val ml_source =
       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
-      "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
-      "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
+      "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^
+      "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^
       "; Test.main ();"
   in
     check_settings compiler ISABELLE_SMLNJ "SMLNJ executable";
isabelle