--- a/src/Pure/General/rat.ML Wed Jun 01 15:33:45 2016 +0200
+++ b/src/Pure/General/rat.ML Wed Jun 01 16:02:02 2016 +0200
@@ -108,3 +108,5 @@
ML_system_overload (fn (a, b) => Rat.lt b a) ">";
ML_system_overload (fn (a, b) => Rat.le b a) ">=";
ML_system_overload (not o Rat.eq) "<>";
+
+ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));
--- a/src/Pure/ROOT.ML Wed Jun 01 15:33:45 2016 +0200
+++ b/src/Pure/ROOT.ML Wed Jun 01 16:02:02 2016 +0200
@@ -52,7 +52,6 @@
subsection "Library of general tools";
ML_file "General/integer.ML";
-ML_file "General/rat.ML";
ML_file "General/stack.ML";
ML_file "General/queue.ML";
ML_file "General/heap.ML";
@@ -62,6 +61,7 @@
ML_file "General/linear_set.ML";
ML_file "General/buffer.ML";
ML_file "General/pretty.ML";
+ML_file "General/rat.ML";
ML_file "PIDE/xml.ML";
ML_file "General/path.ML";
ML_file "General/url.ML";