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/Pure/Isar/proof.ML
changeset 80809 4a64fc4d1cde
parent 79113 5109e4b2a292
child 80873 e71cb37c7395 
--- a/src/Pure/Isar/proof.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -180,8 +180,7 @@
       (context * thm list list -> context -> context)};
 
 val _ =
-  ML_system_pp (fn _ => fn _ => fn _: state =>
-    Pretty.to_polyml (Pretty.str "<Proof.state>"));
+  ML_system_pp (fn _ => fn _ => fn _: state => ML_Pretty.str "<Proof.state>");
 
 fun make_goal (statement, using, goal, before_qed, after_qed) =
   Goal {statement = statement, using = using, goal = goal,
isabelle