# HG changeset patch
# User wenzelm
# Date 1464875565 -7200
# Node ID 06cbfbaf39c5666ec210f96cdba3af3417f0ef6e
# Parent  a5697f7a33223c860c18538d9c01da45b349fe2f
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;

diff -r a5697f7a3322 -r 06cbfbaf39c5 src/Pure/ML_Bootstrap.thy
--- 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>