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.
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
authorwenzelm
Thu, 02 Jun 2016 15:52:45 +0200
changeset 63220 06cbfbaf39c5
parent 63219 a5697f7a3322
child 63221 7d43fbbaba28
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
src/Pure/ML_Bootstrap.thy file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML_Bootstrap.thy	Thu Jun 02 08:34:23 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Thu Jun 02 15:52:45 2016 +0200
@@ -15,6 +15,7 @@
 SML_import \<open>
   structure Output_Primitives = Output_Primitives_Virtual;
   structure Thread_Data = Thread_Data_Virtual;
+  fun ML_system_pp (_: int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
 \<close>
isabelle