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/Tools/literal.ML
changeset 82380 ceb4f33d3073
parent 69593 3dda49e08b9d 
--- a/src/HOL/Tools/literal.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/literal.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -103,7 +103,7 @@
   let
     fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
       case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
-        SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
+        SOME s => (Pretty.str o Code_Printer.literal_string literals) s
       | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
   in
     thy
isabelle