# HG changeset patch
# User wenzelm
# Date 1477041555 -7200
# Node ID abf7b6e6865ffb450ffacabd2e2b97d7a52474d5
# Parent  d9a9ae3956f65b5f9e5db487ace3397632269359
proper type for Poly/ML development version;

diff -r d9a9ae3956f6 -r abf7b6e6865f src/Pure/ML_Bootstrap.thy
--- a/src/Pure/ML_Bootstrap.thy	Fri Oct 21 11:00:16 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Fri Oct 21 11:19:15 2016 +0200
@@ -15,7 +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) = ();
+  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
 \<close>